Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / tests / cocospec / integrator_12BWithoutModesAndInitialization.lus @ 6ccfcb12

History | View | Annotate | Download (2.39 KB)

1
--Historically
2
node H(X:bool) returns (Y:bool);
3
let
4
    Y = X -> (X and (pre Y));
5
tel
6

    
7
--Y since inclusive X
8
node SI(X,Y: bool) returns (Z:bool);
9
let
10
Z = Y and (X or (false -> pre Z));
11
tel
12

    
13
--Y since X
14
node S(X,Y: bool) returns (Z:bool);
15
let
16
Z = X or (Y and (false -> pre Z));
17
tel
18

    
19
--Once
20
node O(X:bool) returns (Y:bool);
21
let
22
 Y = X or (false -> pre Y);
23
tel
24

    
25
node First( X : bool ) returns ( Y : bool );
26
let
27
  Y = X -> pre Y;
28
tel
29

    
30
--Timed Once: less than or equal to N
31
node OTlore(const N: int; X: bool; ) returns (Y: bool);
32
    var C:int;
33
let
34
    C = if X then 0
35
        else (-1 -> pre C + (if pre C <0 then 0 else 1));
36

    
37
    Y = First(X)
38
        ->
39
        (if pre C < 0  then false
40
         else C <= N
41
        );
42
tel
43

    
44
-- Timed Historically: less than or equal to N
45
node HTlore(const N: int; X: bool) returns (Y: bool);
46
let
47
  Y = not OTlore(N, not X);
48
tel
49

    
50
-- Timed Since: less than or equal to N
51
node STlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
52
let
53
  Z = S(X, Y) and OTlore(N, X);
54
tel
55

    
56
-- Timed Since Inclusive: less than or equal to N
57
node SITlore(const N: int; X: bool; Y: bool; )  returns (Z: bool);
58
let
59
  Z = SI(X,Y) and OTlore(N, X);
60
tel
61

    
62
(*@ 
63
contract integrator_12BSpec(BL:real; ic:real; reset:bool; T:real; TL:real; xin:real; ) returns (yout: real; );
64

    
65
--Block Path: integrator_12B
66

    
67
let
68
var FTP:bool = true -> false;
69
var xinpv: real = 0.0 -> pre xin;
70
var ypv: real = 0.0 -> pre yout;
71
var normal: bool = not reset and yout <= TL and yout >= BL;
72
var normal_yout : real = T * 0.5 * ( xin + xinpv ) + ypv;
73
assume BL <=  TL;
74
--assume T > 0.0;
75
guarantee "TUI-002" S( ((yout <= TL and yout >= BL) and FTP), (yout <= TL and yout >= BL) );
76

    
77
guarantee "TUI-001" S((( BL <= ic and ic <= TL ) and reset) => (yout = ic) , (((( BL <= ic and ic <= TL ) and reset) => (yout = ic)) and FTP));
78

    
79
guarantee "TUI-003-V2" normal and ((normal_yout <= TL and normal_yout >= BL)) => yout = normal_yout;
80
guarantee "TUI-003" true -> (H(((( not normal) and (pre ( normal ))) and ( not FTP)) => (pre (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) ))))) and ((S( (( not (( not normal) and (pre ( normal )))) and (normal and (FTP or (pre (  not normal ))))), ( not (( not normal) and (pre ( normal )))) )) => (S( ((yout = T / 2.0 * ( xin + xinpv ) + ypv) and (normal and (FTP or (pre (  not normal ))))), (yout = T / 2.0 * ( xin + xinpv ) + ypv) )));
81

    
82

    
83
tel
84
*)