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