hets/test/Petri.hascasl

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
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
library Petri
version 0.1

from Graphs get Set, Map, SetRepresentation, AbstractSetConstructions1

logic HasCASL

spec Nat = {}


spec MultiSet = Nat and Set then
  var Elem : Type
  type  MultiSet Elem = Elem ->? Nat
then %def
  ops __ isIn__ : Pred (Elem * MultiSet Elem);
      __ <= __ : Pred (MultiSet Elem * MultiSet Elem);
      {} : Elem -> MultiSet Elem;
      {__} : Elem -> MultiSet Elem;
      __ + __, __ - __, __intersection__: MultiSet Elem * MultiSet Elem -> MultiSet Elem;
      freq : Elem * MultiSet Elem -> Nat;
      setToMultiSet : Set Elem -> MultiSet Elem

 forall x,y : Elem; B,C,D,E:MultiSet Elem; S: Set Elem

     . freq(x,B) = if def B x then B x else 0     %(freq_def)%
     . freq(x,B + C) = freq(x,B) + freq(x,C)      %(freq_union)%

     . x isIn B <=> freq(x,B) > 0                     %(MultiSet_isIn)%

     . B <= C <=>
       forall x: Elem . freq(x,B) <= freq(x,C)         %(MultiSet_subseteq)%

     . freq (x,setToMultiSet S) = if x isIn S then 1 else 0

     . B intersection C = D <=>
       forall x: Elem . freq(x,D) = min (freq(x,B), freq(x,C))
                                                  %(MultiSet_cap)%
     . B - C = D <=>
           forall x: Elem .
           ( freq(x,B) >= freq(x,C) => freq(x,B) = freq(x,D) + freq(x,C) )
           /\
           ( freq(x,B) <= freq(x,C) => freq(x,D) = 0 )
       %(MultiSet_diff)%
then %implies
  ops __ intersection __: MultiSet Elem * MultiSet Elem -> MultiSet Elem,
                          assoc, comm, idem
end


spec PetriNet =
  Set and Map
then
  sorts P,T
  type Net = {ppp : Set P  *  (T ->? Set P) * (T ->? Set P)
                        . dom pre=dom post /\
                        pre :: dom  pre  -> p /\
                        post :: dom post  -> p }

  op __union__ : Net * Net -> Net

  forall n1,n2:Net
  . n1 union n2 =
    let (p1,pre1,post1) = n1
        (p2,pre2,post2) = n2
    in (p1 union p2,
        \t:T . if def pre1(t) then if def pre2(t) then pre1(t) + pre2(t)
                                                else pre1(t)
                            else pre2(t),
        \t:T . if def post1(t) then if def post2(t) then post1(t) + post2(t)
                                                  else post1(t)
                            else post2(t))
        as Net
end


spec PetriSystem =
  MultiSet and PetriNet
then
  type Marking = MultiSet P
  type System = {nm : Net * Marking
                          . let (p,pre,post) = n
                            in forall x:P . x isIn m => x isIn p }

  ops  marking   : System ->  Marking;
       net       : System -> Net;
       empty     : Marking;
        __[__]>  : System * T -> System;
       __union__ : System * System -> System

  forall sys,sys1,sys2:System; n:Net; x:P; m:Marking; t:T
  . empty = {}
  . net sys = let (n,m) = sys in n
  . marking sys = let (n,m) = sys in m
  . def sys[t]> <=> (t isIn dom pre
      /\ forall x:P . x isIn pre(t) => x isIn marking(sys))
  . def sys[t]> => sys[t]> = (net(sys),
       marking(sys) - setToMultiSet(pre(t)) + setToMultiSet(post(t)))
           as System
  . sys1 union sys2 =
      (net(sys1) union net(sys2), marking(sys1) + marking(sys2)) as System
end

spec WorkflowNet [SetRepresentation with S |-> P]
                 [SetRepresentation with S |-> T] =
  PetriSystem
and AbstractSetConstructions[SetRepresentation with S |-> P fit S |-> P]
and AbstractSetConstructions[SetRepresentation with T |-> P fit T |-> P]
then
  type WNet={(sys,i,o): System x P x P .
                 let ((p,pre,post),m) = sys in
                   i isIn p
                /\ o isIn p
                /\ not i isIn range(post)
                /\ not o isIn range(pre) }

  ops input, output : WorkflowNet -> P;
      system : WorkflowNet -> System;
      __union__ : WorkflowNet * WorkflowNet -> WorkflowNet

  forall w,w1,w2:WorkflowNet; sys:System; i,o:P
  . system w = let (sys,i,o) = w in sys
  . input w = let (sys,i,o) = w in i
  . output w = let (sys,i,o) = w in o
  . w1~ union w2 =
    let (((p1,pre1,post1),m1),i1,o1) = w1
        (((p2,pre2,post2),m2),i2,o2) = w2
        r = \ (x,y) . x=y \/ (x=inl o1 /\ y=inr i2) \/ (y=inl o1 /\ x=inr i2)
        p = (p1 coproduct p2) factor r
        q = coeq r
        t = (dom pre1)~ coproduct~ (dom pre2)
        pre t = if def left t then image~ (q o inl)~ (pre1 (left t))
                else if def right t then image~ (q o inr)~ (pre2 (right t))
                else undefined
        post t = if def left t then image~ (q o inl)~ (post1 (left t))
                else if def right t then image~ (q o inr)~ (post2 (right t))
                else undefined
        m = map~ (q o inl)~ m1~ +~ map~ (q o inr)~ m2
    in (((p,pre,post),m),i1,o2)~ as WNet
end