Project

General

Profile

« Previous | Next » 

Revision 3debaf88

Added by Pierre-Loïc Garoche about 4 years ago

Removed mode labels

View differences:

tests/cocospec/ElevatorSpec.lus
128 128 
  );
129 129
130 130 
  mode servicing1 (
131 
    require SinceIncl(Call_1, not ::blocked and not Floor_1
131 
    require SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1
132 132 
                              and not (false -> pre MotorUp)
133 133 
                              ) ;
134 134 
    ensure MotorDown ;
......
136 136 
  ) ;
137 137
138 138 
  mode servicing2 (
139 
    require SinceIncl(Call_2, not ::servicing1
140 
                              and not ::blocked and not Floor_2
139 
    require SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1
140 
                              and not (false -> pre MotorUp)))
141 
                              and not (Stop or DoorOpen) and not Floor_2
141 142 
                              and not (false -> pre MotorDown)
142 143 
                              ) ;
143 144 
    ensure MotorUp ;
......
145 146 
  ) ;
146 147 

  		




  147
  148
  
    
 mode waiting (


  		




  148
  
  
    
    require not ::blocked ;


  		




  149
  
  
    
    require not ::servicing1 ;


  		




  150
  
  
    
    require not ::servicing2 ;


  		




  
  149
  
    
    require not (Stop or DoorOpen) ;


  		




  
  150
  
    
    require not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  


  		




  
  151
  
    
                              and not (false -> pre MotorUp))) ;


  		




  
  152
  
    
    require not (SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  


  		




  
  153
  
    
                              and not (false -> pre MotorUp)))  


  		




  
  154
  
    
                              and not (Stop or DoorOpen) and not Floor_2  


  		




  
  155
  
    
                              and not (false -> pre MotorDown) 


  		




  
  156
  
    
                              )) ;


  		




  151
  157
  
    
    ensure not MotorUp ;


  		




  152
  158
  
    
    ensure not MotorDown ;


  		




  153
  159
  
    
  ) ;


  		




  ......




  182
  188
  
    
  -- Guarantees --


  		




  183
  189
  
    
  ----------------


  		




  184
  190
  
    
  -- the execution modes are mutually exclusive  


  		




  185
  
  
    
  guarantee MutuallyExcl_4(::blocked, ::servicing1, ::servicing2, ::waiting) ;


  		




  
  191
  
    
  guarantee MutuallyExcl_4((Stop or DoorOpen), (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  


  		




  
  192
  
    
                              and not (false -> pre MotorUp))), (SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  


  		




  
  193
  
    
                              and not (false -> pre MotorUp)))  


  		




  
  194
  
    
                              and not (Stop or DoorOpen) and not Floor_2  


  		




  
  195
  
    
                              and not (false -> pre MotorDown) 


  		




  
  196
  
    
                              )), (not (Stop or DoorOpen) and 


  		




  
  197
  
    
    not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  


  		




  
  198
  
    
                              and not (false -> pre MotorUp))) and


  		




  
  199
  
    
    not (SinceIncl(Call_2, not (SinceIncl(Call_1, not (Stop or DoorOpen) and not Floor_1  


  		




  
  200
  
    
                              and not (false -> pre MotorUp)))  


  		




  
  201
  
    
                              and not (Stop or DoorOpen) and not Floor_2  


  		




  
  202
  
    
                              and not (false -> pre MotorDown) 


  		




  
  203
  
    
                              )))) ;


  		




  186
  204
  
    

  		




  187
  205
  
    
  -- R1: The elevator moves only when the door is closed and


  		




  188
  206
  
    
  --     the Stop button is not pressed


  		












Also available in:  Unified diff