PetriSystemCategory.hascasl revision 7b47917488ffdd72119358c064c94e5dfc4f8fe3
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco op 0,1 : Nat
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco op __ + __, __-__, min : Nat * Nat -> Nat;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco pred __ >= __, __<=__, __>__ : Nat * Nat
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco free type Boolean ::= True | False
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco var S,V : Type
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco type Set S := S ->? Unit;
a1318a82916028f363b3c5b52e7fd7256b632497Trond Norbye ops emptySet : Set S;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco {__} : S -> Set S;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __isIn__ : S * Set S ->? Unit;
c0550b01024b910b8c1468811c0ea663b10b1372Trond Norbye __subset__ :Pred( Set(S) * Set(S) );
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __union__, __intersection__, __\\__ : Set S * Set S -> Set S;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __disjoint__ : Pred( Set(S) * Set(S) );
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __*__ : Set S * Set V -> Set (S*V);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __disjointUnion__ : Set S * Set S -> Set (S*Boolean);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco injl,injr : S -> S*Boolean;
6d7c6f82e644c205bc679ee5b1fa2929ec949963Lubos Kosco var Elem : Type
67b14513c549ae0027ba7590e736b3dd3281db7cLubos Kosco type MultiSet Elem := Elem ->? Nat
f9fd2b96d1c5ea62664f74da0e34a04b6511a8ffLubos Kosco ops __ isIn__ : Pred (Elem * MultiSet Elem);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __ <= __ : Pred (MultiSet Elem * MultiSet Elem);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco {} : MultiSet Elem;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco {__} : Elem -> MultiSet Elem;
f9fd2b96d1c5ea62664f74da0e34a04b6511a8ffLubos Kosco __ + __, __ - __, __intersection__:
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco MultiSet Elem * MultiSet Elem -> MultiSet Elem;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco freq : Elem * MultiSet Elem -> Nat;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco setToMultiSet : Set Elem -> MultiSet Elem
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco var Elem : Type
a1318a82916028f363b3c5b52e7fd7256b632497Trond Norbye op MultiSetToSet : MultiSet Elem -> Set Elem
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco forall B:MultiSet Elem; S: Set Elem
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco . let S = MultiSetToSet(B) in
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco forall x: Elem. x isIn S <=> freq(x,B) > 0
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco var S : Type
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco type MapMultiSet S := MultiSet S ->? MultiSet S
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco ops sumN : (Nat->?Nat) -> Nat -> Nat;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco sumSet : Set Nat ->? Nat;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco sum : (a->?Nat) -> Pred a ->? Nat
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco var S,V,U : Type
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco type Map S := S->?S
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco ops dom : (S->?V) -> Set S;
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco range : (S->?V) -> Set V;
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco image : (S->?V) -> Set S -> Set V;
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco emptyMap : (S->?V);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __ :: __ --> __ : Pred ( (S->?V) * Pred(S) * Pred(V) );
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __ [__/__] : (S->?V) * S * V -> (S->?V);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __ - __ : (S->?V) * S -> (S->?V);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __o__ : (V->?U) * (S->?V) -> (S->?U);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco __||__ : (S->?V) * Set S -> (S->?V);
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco undef__ : S ->?V;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco ker : (S->?V) -> Pred (S*S);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco injective : Pred(S->?V);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __intersectionMap__, __unionMap__ : (S->?V) * (S->?V) -> (S->?V);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __restrict__ : (S->?V) * Set S -> (S->?V)
87396bac3204b6788c817e19222626eefde8f3f0Knut Anders Hatlen var S, V : Type
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco ops __ :: __ --> __ : Pred ( (S->? MultiSet V) * Set S * Set V);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco freeMap : Map S -> MapMultiSet S;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco linMap : (S->? MultiSet V) -> (MultiSet S->? MultiSet V)
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco ops __ intersection __: MultiSet Elem * MultiSet Elem -> MultiSet Elem,
a1318a82916028f363b3c5b52e7fd7256b632497Trond Norbye assoc, comm, idem
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco type Net = {(p,pre,post) : Set P * (T ->? MultiSet P) * (T ->? MultiSet P) . dom pre=dom post /\
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco (forall p1:MultiSet P . p1 isIn range pre => MultiSetToSet p1 subset p)
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco /\ (forall p1:MultiSet P . p1 isIn range pre => MultiSetToSet p1 subset p) }
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco ops places : Net -> Set P;
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco transitions : Net -> Set T;
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco preMap, postMap : Net -> (T ->? MultiSet P);
05697f2a7c396f7599ba8963ab8179775db4e436Lubos Kosco type HomNet =
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco {(n1,hp,ht,n2) : Net * (P->?P) * (T->?T) * Net .
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco hp :: places n1 --> places n2 /\ ht :: transitions n1 --> transitions n2
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco /\ forall t:T . t isIn transitions n1 =>
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco ( freeMap hp (preMap n1 t) = preMap n2 (ht t)
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco /\ freeMap hp (postMap n1 t) = postMap n2 (ht t) ) }
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco ops dom : HomNet -> Net;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco cod : HomNet -> Net;
7224b1456affc41e89cf46eda1e0b74a044bcc93Lubos Kosco placesMap : HomNet -> (P->?P);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco transitionsMap : HomNet -> (T->?T);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco id : Net ->? HomNet;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __o__ : HomNet * HomNet ->? HomNet
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco pred injective : HomNet
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco type Marking := MultiSet P
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco type System = {(n,m) : Net * Marking
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco . let (p,pre1,post1) = n
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco in forall x:P . x isIn m => x isIn p }
a1318a82916028f363b3c5b52e7fd7256b632497Trond Norbye ops marking : System -> Marking;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco net : System -> Net;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco empty : Marking;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __|<__> : System * T -> System;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __|<__> : System * MultiSet T ->? System;
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco type HomSys = {(sys1,hp,ht,sys2) : System * (P->?P) * (T->?T) * System .
2a335dc8289c2018c8311c41a05286a205e754c4Lubos Kosco ((net(sys1), hp, ht, net(sys2)) in HomNet )
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco /\ forall p: P. freq(p, marking(sys1)) <= freq(hp p, marking(sys2))}
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco ops dom : HomSys -> System;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco cod : HomSys -> System;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco placesMap : HomSys -> (P->?P);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco transitionsMap : HomSys -> (T->?T);
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco id : System ->? HomSys;
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco __o__ : HomSys * HomSys ->? HomSys
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco pred injective : HomSys
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco forall h1, h2:HomSys
a1318a82916028f363b3c5b52e7fd7256b632497Trond Norbye . def (h2 o h1) => h2 o h1 =
fb96d0f1ab431db23ef75c52867d8261acda9b0aLubos Kosco (dom h1, placesMap h2 o placesMap h1, transitionsMap h2 o transitionsMap h1,cod h2)