Download code

Jump to: navigation, search

Back to CTL_model_checker_(CSP)

Download for Windows: single file, zip

Download for UNIX: single file, zip, tar.gz, tar.bz2

ctl_model_checker.csp

  1 const_MaxState = 10
  2 datatype STATE = S.{0..const_MaxState}
  3 
  4 -- A set of states
  5 States = { S.0, S.1, S.2, S.3 }
  6 
  7 -- A set of transitions
  8 Trans = { (S.0, S.2), 
  9           (S.0, S.3),
 10           (S.1, S.0),
 11           (S.2, S.3),
 12           (S.3, S.0),
 13           (S.3, S.1) }
 14           
 15 -- A labeling function
 16 Labels = { (S.0, {Atom.A, Atom.C}),
 17            (S.1, {Atom.C}),
 18            (S.2, {Atom.A, Atom.B}),
 19            (S.3, {Atom.B}) }
 20 
 21 
 22 Spec1 = EX.Atom.B
 23 Spec2 = EU.(And.(Atom.A, Atom.B), Atom.C)
 24 Spec3 = AF.Not.Atom.C
 25 Spec4 = EX.Atom.C
 26 Spec5 = AU.(Atom.C, And.(Atom.A, Atom.B))
 27 
 28 channel state: STATE
 29 
 30 SAT_States1 = SAT(Spec1)
 31 assert state?s:SAT_States1 -> STOP [T= state!S.0 -> STOP 
 32 
 33 SAT_States2 = SAT(Spec2)
 34 assert state?s:SAT_States2 -> STOP [T= state!S.0 -> STOP 
 35 
 36 SAT_States3 = SAT(Spec3)
 37 assert state?s:SAT_States3 -> STOP [T= state!S.0 -> STOP 
 38 
 39 SAT_States4 = SAT(Spec4)
 40 assert not state?s:SAT_States4 -> STOP [T= state!S.0 -> STOP
 41 
 42 SAT_States5 = SAT(Spec5)
 43 assert not state?s:SAT_States5 -> STOP [T= state!S.0 -> STOP
 44 
 45 datatype ATOM = A | B | C | D
 46 
 47 datatype CTL_FORMULA 
 48     = Top
 49     | Bottom
 50     | Atom.ATOM
 51     | Not.CTL_FORMULA    
 52     | And.(CTL_FORMULA, CTL_FORMULA)
 53     | Or.(CTL_FORMULA, CTL_FORMULA)
 54     | Implic.(CTL_FORMULA, CTL_FORMULA)
 55     | AX.CTL_FORMULA
 56     | EX.CTL_FORMULA
 57     | AU.(CTL_FORMULA, CTL_FORMULA)
 58     | EU.(CTL_FORMULA, CTL_FORMULA)
 59     | EF.CTL_FORMULA
 60     | EG.CTL_FORMULA
 61     | AF.CTL_FORMULA
 62     | AG.CTL_FORMULA
 63 
 64 SAT(Top) = States
 65 SAT(Bottom) = {}
 66 SAT(Atom.p) = { s | (s, L) <- Labels, member(Atom.p, L) }
 67 SAT(Not.p) = diff(States, SAT(p))
 68 SAT(And.(p, q)) = inter(SAT(p), SAT(q))
 69 SAT(Or.(p, q)) = union(SAT(p), SAT(q))
 70 SAT(Implic.(p, q)) = SAT(Or.(Not.p, q))
 71 SAT(AX.p) = SAT(Not.EX.Not.p)
 72 SAT(EX.p) = SAT_EX(p)
 73 SAT(AU.(p, q)) = SAT(Not.Or.(EU.(Not.p, And.(Not.p, Not.q)), EG.Not.q))
 74 SAT(EU.(p, q)) = SAT_EU(p, q)
 75 SAT(EF.p) = SAT(EU.(Top, p))
 76 SAT(EG.p) = SAT(Not.AF.Not.p)
 77 SAT(AF.p) = SAT_AF(p)
 78 SAT(AG.p) = SAT(Not.EF.Not.p)
 79 
 80 SAT_EX(p) = 
 81     let
 82         X = SAT(p)
 83     within
 84         pre_E(X)
 85         
 86 SAT_AF(p) = 
 87     let
 88         Y = SAT(p)
 89         f(X) = union(X, pre_A(X))
 90     within
 91         if Y == States
 92         then Y
 93         else Fixpoint(f, Y)
 94         
 95 SAT_EU(p,q) = 
 96     let
 97         W = SAT(p)
 98         Y = SAT(q)
 99         f(X) = union(X, inter(W, pre_E(X)))
100     within
101         if Y == States
102         then Y
103         else Fixpoint(f, Y)
104         
105 pre_E(X) = { s0 | (s0, s1) <- Trans, member(s1, X) }
106 pre_A(X) = diff( pre_E(X), pre_E( diff(States, X) ) )
107 Fixpoint(f, X) = 
108     let
109         X' = f(X)
110     within
111         if X == X'
112         then X
113         else Fixpoint(f, X')


hijacker
hijacker
hijacker
hijacker