forked from Callmejp/CCSL2Maude
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathccsl.maude
97 lines (81 loc) · 2.8 KB
/
ccsl.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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
fmod CLOCK is
including QID .
including BOOL .
sorts Clock ClockSet .
subsort Qid < Clock < ClockSet .
op empty : -> Clock .
op _,_ : ClockSet ClockSet -> ClockSet [ctor assoc comm id: empty] .
op _in_ : Clock ClockSet -> Bool .
vars C1 C2 : Clock .
var CS1 : ClockSet .
eq C1 in empty = false .
eq C1 in (C2, CS1) =
if (C1 == C2) then true else C1 in CS1 fi .
endfm
fmod TICK-LIST is
sort TickList .
ops nil : -> TickList .
op _,i : TickList -> TickList .
op _,t : TickList -> TickList .
endfm
fmod CONSTRAINTS is
including CLOCK .
including NAT .
sorts Constraint Constraints .
subsort Constraint < Constraints .
op empty : -> Constraints [ctor] .
op __ : Constraints Constraints -> Constraints [ctor assoc comm id: empty] .
op _<_ : Clock Clock -> Constraint [ctor] .
op _!=_$_ : Clock Clock Nat -> Constraint [ctor] .
op _!=_+_ : Clock Clock Clock -> Constraint [ctor] .
op _!=_*_ : Clock Clock Clock -> Constraint [ctor] .
op _!=_/\_ : Clock Clock Clock -> Constraint [ctor] .
op _!=_\/_ : Clock Clock Clock -> Constraint [ctor] .
op _<<_ : Clock Clock -> Constraint [ctor] .
op _#_ : Clock Clock -> Constraint [ctor] .
op _<=_ : Clock Clock -> Constraint [ctor] .
op _!=_~_ : Clock Clock Clock -> Constraint [ctor] .
endfm
fmod CONFIGURATION is
including NAT + CLOCK + TICK-LIST .
sort ConfElt Conf .
subsort ConfElt < Conf .
op [_,_,_] : Clock TickList Nat -> ConfElt [ctor] .
op empty : -> Conf [ctor] .
op _,_ : Conf Conf -> Conf [ctor assoc comm id: empty] .
endfm
mod MAIN is
including BOOL .
including CLOCK .
including NAT .
including CONSTRAINTS .
including CONFIGURATION .
including TICK-LIST .
sort CCSLState .
op <_;_;_;_> : ClockSet Constraints Conf Nat -> CCSLState [ctor] .
op satisfy : ClockSet Conf Constraint -> Bool .
vars F F' : ClockSet .
var CON : Constraint .
var PHI : Constraints .
var X : Conf .
var Y : ConfElt .
vars K N N1 N2 : Nat .
vars C1 C2 : Clock .
vars TL1 TL2 : TickList .
--- General
eq satisfy(F, X, empty) = true .
--- Precedence
eq satisfy(F, ([C1, TL1, N1], [C2, TL2, N2], X), C1 < C2) =
if N1 == N2 then not (C2 in F) else true fi .
--- Delay
eq satisfy(F, ([C2, TL2, N2], X), C1 != C2 $ N) =
if N2 >= N then (C1 in F) == (C2 in F) else not (C1 in F) fi .
eq satisfy(F, X, (CON PHI)) = if (satisfy(F, X, CON)) then satisfy(F, X, PHI) else false fi .
--- update here
op update : Conf ClockSet -> Conf .
eq update(([C1, TL1, N1], X), F) =
if (C1 in F) then ([C1, (TL1, t), N1 + 1], update(X, F)) else ([C1, (TL1, i), N1], update(X, F)) fi .
eq update(empty, F) = empty .
crl < (F, F') ; PHI ; X ; K > => < (F, F') ; PHI ; update(X, F) ; K + 1 >
if F =/= empty /\ satisfy(F, X, PHI) .
endm