-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathbitml-test.maude
55 lines (36 loc) · 1.25 KB
/
bitml-test.maude
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
mod TEST is
protecting BITML .
ops A B C : -> Participant .
ops X Y Z : -> ContractName .
ops Contr Contr1 Contr2 Contr3 Contr4 : -> Configuration .
***ops test : -> Contract .
***eq dec = (X := wd A), (Y := wd B) .
eq dec = (X := (rngt X) + (wd C)), (Y := (rngt Y)) .
eq Contr = < tau. wd A + (wd B)> | unlock .
eq Contr1 = < split( (wd A) (wd B)) > | unlock .
eq Contr2 = < *: tau. wd A > | unlock .
eq Contr3 = < rngt X + (wd B)> | unlock | X .
eq Contr4 = unlock | < wd C + rngt Y > | Y .
endm
***rew Contr .
***rew Contr1 .
***rew Contr2 .
***rew Contr3 .
search Contr3 =>* G:Configuration .
***search Contr =>* G:Configuration .
*** red (|| test) .
***red dec .
***red ref X dec .
***red isDeclared X dec .
***red isDeclared Z dec .
***red isExpanded X Contr3 | X.
***red isExpanded X Contr3 .
smod LIQUIDITY-CHECK is
protecting BITML_CHECK .
including TEST .
endsm
reduce in LIQUIDITY-CHECK : modelCheck(Contr1 , <> contract-free) . *** true
reduce in LIQUIDITY-CHECK : modelCheck(Contr3 , <> contract-free) . *** true
reduce in LIQUIDITY-CHECK : modelCheck(Contr4 , <> contract-free) . *** false
***search Contr3 =>* G:Configuration .
quit .