Subversion

AlloyUML

?curdirlinks? - Rev 52

?prevdifflink? - Blame 



context  Course 
 inv:  
 Lab .allInstances() -> select(  y0  |  (self . labsC -> includes(y0)) ) ->size() >= 1


context  Course 
 inv:  ( ( (self . optional -> includes(self))  and  
 Course .allInstances() -> forAll (  v0  |  ( (v0 . optional -> includes(v0))  implies  (v0 = self) ) )  )  implies  
 Lab .allInstances() -> exists (  v1  |  ( (self . labsC -> includes(v1))  and  (v1 . type -> includes(TypeLab::Practical)) ) )  )


context  Course 
 inv:  
 Lab .allInstances() -> exists (  l  |  ( (self . labsC -> includes(l))  and  ( 
 TypeLab .allInstances() -> forAll (  v0  |  ( (l . type -> includes(v0))  implies  (v0 = TypeLab :: Theorical) ) )   and  (l . type -> includes(TypeLab::Theorical)) ) ) ) 


context  Student :: isEnrolled () : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() >= 1 


context  Student :: enroll (c:Course) : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() = 0 
pre:  not ( (self . passed -> includes(c)) ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current -> includes(v1))  implies  ( (v0 . current@pre -> includes(v1))  or  ( (v0 = self)  and  (v1 = c) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . current@pre -> includes(v1))  or  ( (v0 = self)  and  (v1 = c) ) )  implies  (v0 . current -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed -> includes(v1))  implies  (v0 . passed@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed@pre -> includes(v1))  implies  (v0 . passed -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs -> includes(v1))  implies  (v0 . labs@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs@pre -> includes(v1))  implies  (v0 . labs -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams -> includes(v1))  implies  (v0 . exams@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams@pre -> includes(v1))  implies  (v0 . exams -> includes(v1)) ) )  )  ) 


context  Student :: lab (l:Lab) : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() >= 1 
pre:  not ( (self . labs -> includes(l)) ) 
pre:  
 Course .allInstances() -> exists (  v1  |  ( (self . current -> includes(v1))  and  (v1 . labsC -> includes(l)) ) )  
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed -> includes(v1))  implies  (v0 . passed@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed@pre -> includes(v1))  implies  (v0 . passed -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current -> includes(v1))  implies  (v0 . current@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current@pre -> includes(v1))  implies  (v0 . current -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs -> includes(v1))  implies  ( (v0 . labs@pre -> includes(v1))  or  ( (v0 = self)  and  (v1 = l) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( ( (v0 . labs@pre -> includes(v1))  or  ( (v0 = self)  and  (v1 = l) ) )  implies  (v0 . labs -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams -> includes(v1))  implies  (v0 . exams@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams@pre -> includes(v1))  implies  (v0 . exams -> includes(v1)) ) )  )  ) 


context  Student :: approve () : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() >= 1 
pre:  not ( 
 Course .allInstances() -> forAll (  v0  |  ( (self . current -> includes(v0))  implies  (self . exams -> includes(v0)) ) )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed -> includes(v1))  implies  (v0 . passed@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed@pre -> includes(v1))  implies  (v0 . passed -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current -> includes(v1))  implies  (v0 . current@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current@pre -> includes(v1))  implies  (v0 . current -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs -> includes(v1))  implies  (v0 . labs@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs@pre -> includes(v1))  implies  (v0 . labs -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams -> includes(v1))  implies  ( (v0 . exams@pre -> includes(v1))  or  ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . exams@pre -> includes(v1))  or  ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) )  implies  (v0 . exams -> includes(v1)) ) )  )  ) 


context  Student :: pass () : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() >= 1 
pre:  
 Course .allInstances() -> forAll (  v0  |  ( (self . current -> includes(v0))  implies  (self . exams -> includes(v0)) ) )  
pre:  
 Lab .allInstances() -> forAll (  v0  |  ( 
 Course .allInstances() -> exists (  v1  |  ( (self . current -> includes(v1))  and  (v1 . labsC -> includes(v0)) ) )   implies  (self . labs -> includes(v0)) ) )  
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams -> includes(v1))  implies  (v0 . exams@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams@pre -> includes(v1))  implies  (v0 . exams -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs -> includes(v1))  implies  (v0 . labs@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs@pre -> includes(v1))  implies  (v0 . labs -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed -> includes(v1))  implies  ( (v0 . passed@pre -> includes(v1))  or  ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . passed@pre -> includes(v1))  or  ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) )  implies  (v0 . passed -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current -> includes(v1))  implies  ( (v0 . current@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (Course .allInstances() -> includes( v1 )) ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . current@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (Course .allInstances() -> includes( v1 )) ) ) )  implies  (v0 . current -> includes(v1)) ) )  )  ) 


context  Student :: quit () : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() >= 1 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams -> includes(v1))  implies  ( (v0 . exams@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . exams@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) ) )  implies  (v0 . exams -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs -> includes(v1))  implies  ( (v0 . labs@pre -> includes(v1))  and  not ( ( (v0 = self)  and  
 Course .allInstances() -> exists (  v2  |  ( (self . current@pre -> includes(v2))  and  (v2 . labsC -> includes(v1)) ) )  ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( ( (v0 . labs@pre -> includes(v1))  and  not ( ( (v0 = self)  and  
 Course .allInstances() -> exists (  v2  |  ( (self . current@pre -> includes(v2))  and  (v2 . labsC -> includes(v1)) ) )  ) ) )  implies  (v0 . labs -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed -> includes(v1))  implies  (v0 . passed@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed@pre -> includes(v1))  implies  (v0 . passed -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current -> includes(v1))  implies  ( (v0 . current@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (Course .allInstances() -> includes( v1 )) ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . current@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (Course .allInstances() -> includes( v1 )) ) ) )  implies  (v0 . current -> includes(v1)) ) )  )  ) 


context  Student :: fail () : void 
pre:  
 Course .allInstances() -> select(  y0  |  (self . current -> includes(y0)) ) ->size() >= 1 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . exams -> includes(v1))  implies  ( (v0 . exams@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . exams@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (self . current@pre -> includes(v1)) ) ) )  implies  (v0 . exams -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( (v0 . labs -> includes(v1))  implies  ( (v0 . labs@pre -> includes(v1))  and  not ( ( (v0 = self)  and  
 Course .allInstances() -> exists (  v2  |  ( (self . current@pre -> includes(v2))  and  (v2 . labsC -> includes(v1)) ) )  ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Lab .allInstances() -> forAll (  v1  |  ( ( (v0 . labs@pre -> includes(v1))  and  not ( ( (v0 = self)  and  
 Course .allInstances() -> exists (  v2  |  ( (self . current@pre -> includes(v2))  and  (v2 . labsC -> includes(v1)) ) )  ) ) )  implies  (v0 . labs -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed -> includes(v1))  implies  (v0 . passed@pre -> includes(v1)) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . passed@pre -> includes(v1))  implies  (v0 . passed -> includes(v1)) ) )  )  ) 
post:  ( 
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( (v0 . current -> includes(v1))  implies  ( (v0 . current@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (Course .allInstances() -> includes( v1 )) ) ) ) ) )  )   and  
 Student .allInstances() -> forAll (  v0  |  
 Course .allInstances() -> forAll (  v1  |  ( ( (v0 . current@pre -> includes(v1))  and  not ( ( (v0 = self)  and  (Course .allInstances() -> includes( v1 )) ) ) )  implies  (v0 . current -> includes(v1)) ) )  )  )
Theme by Vikram Singh | Powered by WebSVN v2.3.3