Project

General

Profile

Revision fd5381b7

View differences:

tests/cocospec/StopwatchSpec.lus
1
-------------------------
2
-- Auxiliary operators --
3
-------------------------
4
node Even (N: int) returns (B: bool) ;
5
let
6
  B = (N mod 2 = 0) ; 
7
tel
8

  
9
node ToInt (X: bool) returns (N: int) ;
10
let
11
  N = if X then 1 else 0 ;
12
tel
13

  
14
node Count (X: bool) returns (N: int) ;
15
let
16
  N = ToInt(X) -> ToInt(X) + pre N ;  
17
tel
18

  
19
node Sofar ( X : bool ) returns ( Y : bool ) ;
20
let
21
 Y = X -> (X and (pre Y)) ;
22
tel
23

  
24
node Since ( X, Y : bool ) returns ( Z : bool ) ;
25
let
26
  Z =  X or (Y and (false -> pre Z)) ;
27
tel
28

  
29

  
30
node SinceIncl ( X, Y : bool ) returns ( Z : bool ) ;
31
let
32
  Z =  Y and (X or (false -> pre Z)) ;
33
tel
34

  
35
node Increased (N: int) returns (B: bool) ;
36
let
37
  B = true -> N > pre N ;
38
tel
39

  
40
node Stable (N: int) returns (B: bool) ;
41
let
42
  B = true -> N = pre N ;
43
tel
44

  
45
-------------------------------
46
-- Stopwatch high-level spec --
47
-------------------------------
48
contract stopwatchSpec ( toggle, reset : bool ) returns ( time : int ) ;
49
let
50
  -- the watch is activated initially if the toggle button is pressed
51
  -- afterwards, it is activated iff 
52
  --   it was activated before and the toggle button is unpressed or
53
  --   it was not activated before and the toggle button is pressed 
54
  var on: bool = toggle ->    (pre on and not toggle) 
55
                           or (not pre on and toggle) ;
56
  
57
  -- we can assume that the two buttons are never pressed together
58
  assume not (toggle and reset) ; 
59
  
60
  -- the elapsed time starts at 1 or 0 depending 
61
  -- on whether the watch is activated or not
62
  guarantee (on => time = 1) -> true ;
63
  guarantee (not on => time = 0) -> true ;
64
  -- the elapsed time is always non-negative
65
  guarantee time >= 0 ;
66
  
67
  -- if there is no reset now and there was an even number of counts since the last reset
68
  -- then the current elapsed time is the same as the previous one
69
  guarantee not reset and Since(reset, Even(Count(toggle))) 
70
            => Stable(time) ;
71
  -- if there is no reset now and there was an odd number of counts since the last reset
72
  -- then the current elapsed time is greater than previous one
73
  guarantee not reset and Since(reset, not Even(Count(toggle))) 
74
            => Increased(time) ;
75

  
76

  
77
--  guarantee true -> not Even(Count(toggle)) and Count(reset) = 0 => time > pre time ;
78

  
79
  
80
  -- the watch is in resetting mode if the reset button is pressed
81
  -- while in that mode, the elapsed time is 0
82
  mode resetting ( 
83
    require reset ; 
84
    ensure time = 0 ; 
85
  ) ;
86

  
87
  -- the watch is in running mode if is activated and 
88
  -- the reset button is unpressed.
89
  -- while in that mode, the elapsed time increases by 1
90
  mode running ( 
91
    require on ; 
92
    require not reset ; 
93
    ensure true -> time = pre time + 1 ; 
94
  ) ;
95

  
96
  -- the watch is in stopped mode if is not activated and 
97
  -- the reset button is unpressed
98
  -- while in that mode, the elapsed time remains the same
99
  mode stopped ( 
100
    require not reset ; 
101
    require not on ; 
102
    ensure true -> time = pre time ; 
103
  ) ;
104
tel
105

  
106
------------------------------
107
-- Stopwatch low-level spec --
108
------------------------------
109

  
110
node stopwatch ( toggle, reset : bool ) returns ( count : int );
111
(*@contract import stopwatchSpec(toggle, reset ) returns (count) ; *)
112
  var running : bool;
113
let
114
  running = (false -> pre running) <> toggle ;
115
  count =
116
    if reset then 0
117
    else if running then 1 -> pre count + 1
118
    else 0 -> pre count ;
119
tel
120

  
121

  
122

  
123

  
124

  
tests/zustre/simple_counter_cex.lus
1 1
node top (reset: bool) returns (ok: bool)
2 2
var  cpt: int;
3 3
let
4
   cpt = 0 -> if reset then 0 else 1 + pre cpt;
4
   cpt = if reset then 3 else 0 -> if reset then 0 else 1 + pre cpt;
5 5
   ok = cpt <> 2;  
6 6
tel

Also available in: Unified diff