library HasCASL/PetriSystem

%%from HasCASL/Set get SetRepresentation, AbstractSetConstructions
from HasCASL/MultiSet get MapMultiSet
from HasCASL/Petri get PetriNet, PetriNetCategory
from HasCASL/HLR get HLRCategory


logic HasCASL

spec PetriSystem = 
  MapMultiSet and PetriNet
then
  type Marking := MultiSet P
  type System = {(n,m) : Net * Marking 
                          . let (p,pre1,post1) = n 
		          in forall x:P . x isIn m => x isIn p }
  ops  marking   : System -> Marking;
       net       : System -> Net;
       empty     : Marking;
       __|<__>   : System * T -> System; 
       __|<__>   : System * MultiSet T ->? System;
  forall sys,sys1,sys2:System; n:Net; m:Marking; t:T; v: MultiSet T 
  . empty = {}
  . net sys = let (n,m) = sys in n
  . marking sys = let (n,m) = sys in m
  . def sys|<t> <=> t isIn (dom (preMap(net(sys)))) /\  preMap(net(sys))  t <= marking(sys)
  . def sys|<t> => sys|<t> = (net(sys), (marking(sys) -  preMap(net(sys)) t) + postMap(net(sys)) t)
  . def sys|<v> <=> forall t:T . t isIn v /\ t isIn (dom (preMap(net(sys)))) /\ linMap (preMap(net(sys))) v <= marking(sys)
  . def sys|<v> => 
    sys|<v> = (net(sys), (marking(sys) - linMap (preMap(net(sys))) v) + linMap (postMap(net(sys))) v )
end

spec PetriSystemCategory = 
  PetriSystem and PetriNetCategory hide M
then
  type HomSys  = {(sys1,hp,ht,sys2) : System  * (P->?P) * (T->?T) * System .  
                  ((net(sys1), hp, ht, net(sys2)) in HomNet )
       /\ forall p: P. freq(p, marking(sys1)) <= freq(hp p, marking(sys2))} 
  ops  dom : HomSys  -> System;
       cod : HomSys  -> System;
       placesMap : HomSys  -> (P->?P);
       transitionsMap : HomSys  -> (T->?T);
       id : System -> HomSys;
       __o__ : HomSys  * HomSys  ->? HomSys 
  pred injective : HomSys
  forall sys,sys1,sys2:System; n:Net; x:P; m:Marking; t:T; hp:P->?P; ht:T->?T; h, h1, h2:HomSys; v: MultiSet T 
  . let (sys1,hp,ht,sys2)=h in dom (h) = sys1
  . let (sys1,hp,ht,sys2)=h in cod (h) = sys2
  . let (sys1,hp,ht,sys2)=h in placesMap (h) = hp
  . let (sys1,hp,ht,sys2)=h in transitionsMap (h) = ht
  . def (h2 o h1) <=> cod h1 = dom h2
  . def (h2 o h1) => h2 o h1 = 
     (dom h1, placesMap h2 o placesMap h1, transitionsMap h2 o transitionsMap h1,cod h2)
      as HomSys
  . injective h <=> injective(placesMap h) /\ injective(transitionsMap h)
  sort M = {h:HomSys . injective h}
end

view CategoryofPetriSystems : HLRCategory to PetriSystemCategory =
     Ob |-> System, Mor |-> HomSys, __o__, dom, cod, id, M
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
]%