**** defined pnets and basic operations there on
fmod PETRI is
  inc QID-LIST .
  inc DISH-OPS .
  inc SIMPLE .    **** for rulenamelists

  sort PNTrans .
****           rid in   out  both
  op pnTrans : Qid Occs Occs Occs -> PNTrans [ctor] .

  sorts PNet PNTransList .
  subsort  PNTrans < PNTransList .

  op nil : -> PNTransList [ctor] .
  op  __ : PNTransList PNTransList -> PNTransList [ctor assoc id: nil] .
  op pnet : PNTransList Occs -> PNet [ctor] .

  var occ : Occ .  vars occs ioccs ooccs boccs preOccs postOccs : Occs .
  vars pntl pntl' pntl0 pntl1 : PNTransList .
  vars pnt pnt' : PNTrans .
  var rid : Qid .
  vars rnl rnl0 : RuleNameList .
  var n : Nat .

  vars kbtl kbtl' : PNTransList .
  vars xoccs newoccs same seenu seend openu opend 
       xoccs' seenu' seend' openu' opend' : Occs .

  op pnt2rid : PNTrans -> Qid .
  ops pnt2pre pnt2post pnt2i pnt2o pnt2b : PNTrans -> Occs .

  eq pnt2rid(pnTrans(rid,ioccs,ooccs,boccs)) = rid .
  eq pnt2pre(pnTrans(rid,ioccs,ooccs,boccs)) = addOccs(ioccs,boccs) .
  eq pnt2post(pnTrans(rid,ioccs,ooccs,boccs)) = addOccs(ooccs,boccs) .
  eq pnt2i(pnTrans(rid,ioccs,ooccs,boccs)) = ioccs .
  eq pnt2o(pnTrans(rid,ioccs,ooccs,boccs)) = ooccs .
  eq pnt2b(pnTrans(rid,ioccs,ooccs,boccs)) = boccs .

  op mkPNTrans : Qid Occs Occs -> PNTrans .
  ceq mkPNTrans(rid,preOccs,postOccs) = pnTrans(rid,ioccs,ooccs,boccs)
  if ioccs := Odiff(preOccs,postOccs)
  /\ ooccs := Odiff(postOccs,preOccs)
  /\ boccs := Osame(postOccs,preOccs) .

  op pntl2rids : PNTransList -> QidList .
  eq pntl2rids(pnt pntl) = pnt2rid(pnt) pntl2rids(pntl) .
  eq pntl2rids(nil) = nil .

  op pnetInit : PNet -> Occs .
  op pnetTrans : PNet -> PNTransList .

  eq pnetInit(pnet(pntl,occs)) = occs .
  eq pnetTrans(pnet(pntl,occs)) = pntl .

  op len : PNTransList -> Nat .
  op lenX : PNTransList Nat -> Nat .
  eq len(pntl) = lenX(pntl,0) .
  eq lenX(nil,n) = n .
  eq lenX(pnt pntl,n) = lenX(pntl,s n) .

  ops getPre getPost : Nat PNTransList -> PNTransList .
  **** getPre(n,L) is prefix of L of length min(n, len(L))
  eq getPre(0, pntl) = nil .
  eq getPre(s n,  nil) = nil .
  eq getPre(s n, pnt pntl) = (pnt getPre(n,pntl) ) .

  **** getPost(n,L) is L' such that L = getPre(n,L) L'
  eq getPost(0, pntl) = pntl .
  eq getPost(s n, nil) = nil .
  eq getPost(s n,  pnt pntl) = getPost(n, pntl) .

  op onlyUsed : PNet -> Occs .
  op onlyUsed : PNTransList Occs  -> Occs .

**** Those init occs that appear as inputs to transitions
  op Used : PNTransList Occ  -> Occs .    **** 0 or 1

  eq onlyUsed(pnet(pntl,occs)) = onlyUsed(pntl,occs) .
  eq onlyUsed(pntl,none) = none .
  eq onlyUsed(pntl, occ occs) = (Used(pntl,occ) onlyUsed(pntl,occs)) .

  eq  Used(nil,occ) = none .
  eq  Used(pnt pntl, occ)
       = ( if (member(occ, pnt2pre(pnt)) =/= none)
           then occ
           else Used(pntl,occ)
           fi ) .

**** all occs occurring in in/out places
  op allOccs : PNTransList -> Occs .
  op allOccsX : PNTransList Occs -> Occs .

  eq allOccs(pntl) = allOccsX(pntl,none) .
  eq allOccsX(nil,occs) = occs .
  eq allOccsX(pnTrans(rid, ioccs,ooccs,boccs) pntl,occs) =
        allOccsX(pntl, addOccs(addOccs(addOccs(occs,ioccs),ooccs),boccs)) .

**** all occs occurring in in/both places
  op allIn : PNTransList -> Occs .
  op allInX : PNTransList Occs -> Occs .

  eq allIn(pntl) = allInX(pntl,none) .
  eq allInX(nil,occs) = occs .
  eq allInX(pnTrans(rid, ioccs,ooccs,boccs) pntl,occs) =
        allInX(pntl, addOccs(ioccs boccs,occs)) .

**** all occs occurring in out places  
  op allOut : PNTransList -> Occs .
  op allOutX : PNTransList Occs -> Occs .

  eq allOut(pntl) = allOutX(pntl,none) .
  eq allOutX(nil,occs) = occs .
  eq allOutX(pnTrans(rid, ioccs,ooccs,boccs) pntl,occs) =
        allOutX(pntl, addOccs(ooccs,occs)) .
  

  op notUsed : PNet -> Occs .
  op notUsed : PNTransList Occs -> Occs .

  eq notUsed(pnet(pntl,occs)) = notUsed(pntl,occs) .
  eq notUsed(pntl,none) = none .
  eq notUsed(pntl, occ occs) =
     ((if (Used(pntl,occ) == occ) then none else occ fi)
      notUsed(pntl,occs)) .

**** rnamelist is shorter -- cdr through it
  op getTrans : PNTransList RuleNameList -> PNTransList .

  eq getTrans(pntl' pnTrans(rid,ioccs,ooccs,boccs) pntl, rid rnl) =
       pnTrans(rid,ioccs,ooccs,boccs)  getTrans(pntl' pntl, rnl)  .

  eq getTrans(pntl,nil) = nil .
  eq getTrans(pntl, rid rnl) =  getTrans(pntl, rnl) [owise] .

**** 07may06
**** add elements of second to first if not already there
  op unionTrans : PNTransList PNTransList -> PNTransList .
  eq unionTrans(pntl, pnTrans(rid,ioccs,ooccs,boccs) pntl') =
      unionTrans(pntl (if getTrans(pntl,rid) == nil 
                       then pnTrans(rid,ioccs,ooccs,boccs)
                       else nil fi),
                 pntl') .

  eq unionTrans(pntl, nil) = pntl .

**** assumes uniform pnt representation      
  op intersectTrans : PNTransList PNTransList -> PNTransList .
  eq intersectTrans( nil, pntl) = nil .
  eq intersectTrans( pnt pntl, pntl0 pnt pntl1) =
       pnt intersectTrans(pntl, pntl0 pntl1) .
  eq intersectTrans( pnt pntl, pntl0 pntl1) =
        intersectTrans(pntl, pntl0 pntl1) [owise] .

**** pntl - pntl'
  op intersectTransC : PNTransList PNTransList -> PNTransList .
  eq intersectTransC( nil, pntl') = nil .
  eq intersectTransC( pnt pntl, pntl0 pnt pntl1) =
        intersectTransC(pntl, pntl0  pntl1) .
  eq intersectTransC( pnt pntl, pntl0 pntl1) =
       pnt intersectTransC(pntl, pntl0 pntl1) [owise] .
    

****************************************************************************
**** for incremental pnet exploration
****************************************************************************
****  XState ~ PNTransList PNTransList PNTransList PNTransList 
****           Occs Occs Occs Occs
  sort XState . 
  op xstate : PNTransList PNTransList PNTransList PNTransList
               Occs Occs Occs Occs -> XState [ctor] .
  sort PNTLPair .
  op `{_,_`} : PNTransList PNTransList -> PNTLPair [ctor] .

  sort Occs4Tuple .
  op `{_,_,_,_`} :  Occs Occs Occs Occs -> Occs4Tuple [ctor] .

  vars scope xnet scope' xnet' new new'  hidden hidden' : PNTransList .
  vars scope1 scope2 scope3 new1 new2 new3 new4 : PNTransList .
  vars sOccs uOccs dOccs bOccs sOccs' uOccs' dOccs' bOccs' : Occs .
  vars inOccs outOccs : Occs .
  vars rids : QidList .
  var xst : XState .

 ops xscope xhidden xnet xnew : XState -> PNTransList .
 ops xseen xup xdn xboth : XState -> Occs .

 eq xscope(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = scope .
 eq xnet(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = xnet .
 eq xnew(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = new .

 eq xhidden(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = hidden .
 eq xseen(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = sOccs .
 eq xup(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = uOccs .
 eq xdn(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = dOccs .
 eq xboth(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = bOccs .



**** partition occs of xnet: uOccs -- open for up,   dOccs open for down
****         bOccs open for both  sOccs the rest
  op xSplit : PNTransList PNTransList -> Occs4Tuple .
  ceq xSplit(scope,xnet) = {sOccs,uOccs,dOccs,bOccs}   
    if inOccs := Osame(allOccs(xnet),allIn(scope))
    /\ outOccs :=  Osame(allOccs(xnet),allOut(scope))
    /\ bOccs := Osame(outOccs,inOccs)
    /\ dOccs := Odiff(inOccs,bOccs)
    /\ uOccs := Odiff(outOccs,bOccs)
    /\ sOccs := Odiff(allOccs(xnet),bOccs uOccs dOccs) .

  ops xnetU xnetD xnetB : PNTransList Occs -> PNTLPair .
  ops xnetU1 xnetD1 xnetB1 : PNTransList Occs PNTransList -> PNTLPair .

  eq xnetU(scope,uOccs) = xnetU1(scope,uOccs,nil) .
  eq xnetD(scope,uOccs) = xnetD1(scope,uOccs,nil) .
  eq xnetB(scope,uOccs) = xnetB1(scope,uOccs,nil) .

  eq xnetU1(scope pnTrans(rid,ioccs,occ ooccs,boccs) scope',(occ uOccs),new) =
      xnetU1(scope scope',(occ uOccs),new pnTrans(rid,ioccs,occ ooccs,boccs)) .
  eq xnetU1(scope,(occ uOccs),new) = xnetU1(scope, uOccs,new) [owise] .
  eq xnetU1(scope,none,new) = {scope,new} .

  ceq xnetD1(scope pnTrans(rid,ioccs,ooccs,boccs) scope',(occ uOccs),new) =
       xnetD1(scope scope',(occ uOccs),new pnTrans(rid,ioccs,ooccs,boccs)) 
    if member(occ, ioccs boccs)  == occ .
**** 13oct clt to prevent exploring from enzymes
****    if member(occ, ioccs)  == occ .

  eq xnetD1(scope,(occ uOccs),new) = xnetD1(scope, uOccs,new) [owise] .
  eq xnetD1(scope,none,new) = {scope,new} .

  ceq xnetB1(scope pnTrans(rid,ioccs,ooccs,boccs) scope',(occ uOccs),new) =
       xnetB1(scope scope',(occ uOccs),new pnTrans(rid,ioccs,ooccs,boccs)) 
    if member(occ, ioccs ooccs boccs) == occ .

  eq xnetB1(scope,(occ uOccs),new) = xnetB1(scope, uOccs,new) [owise] .
  eq xnetB1(scope,none,new) = {scope,new} .

**** add split trans with id in rids from scope
  op splitTrans : PNTransList QidList PNTransList -> PNTLPair .

**** assumes at most one transition with given rid
  eq splitTrans(scope,nil,new) = {scope,new} .
  eq splitTrans(scope pnTrans(rid,ioccs,ooccs,boccs) scope',rid rids,new) = 
       splitTrans(scope scope',rids,new pnTrans(rid,ioccs,ooccs,boccs)) .
  eq splitTrans(scope,rid rids,new) = splitTrans(scope,rids,new) [owise] .


  op xsAddRules : PNTransList PNTransList PNTransList QidList -> XState .
  op xsHideRules : PNTransList PNTransList PNTransList QidList -> XState .
  op xsUnHideRules : PNTransList PNTransList PNTransList QidList -> XState .
  op exploreFps : PNTransList PNTransList PNTransList Occs Occs Occs -> XState .
  ops exploreUp1 exploreDn1 : XState -> XState .
  ops exploreUp  exploreDn : XState Nat -> XState .

  ceq xsAddRules(scope,hidden,xnet,rids) =
        xstate(scope1,hidden,xnet new,new,sOccs,uOccs,dOccs,bOccs)
    if {scope1,new} := splitTrans(scope,rids,nil) 
    /\ {sOccs,uOccs,dOccs,bOccs} := xSplit(scope1, xnet new) .

  ceq exploreUp1(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) =
       xstate(scope',hidden,xnet new',new',sOccs',uOccs',dOccs',bOccs')
  if {scope',new'} := xnetU(scope,uOccs bOccs)
  /\ {sOccs',uOccs',dOccs',bOccs'} := xSplit(scope', xnet new') .

  eq exploreUp(xst,0) = xst .
  eq exploreUp(xst,s n) = exploreUp(exploreUp1(xst),n)  .

  ceq exploreDn1(xstate(scope,hidden,xnet,new,sOccs,uOccs,dOccs,bOccs)) = 
     xstate(scope',hidden,xnet new',new',sOccs',uOccs',dOccs',bOccs')
  if {scope',new'} := xnetD(scope,dOccs bOccs)
  /\ {sOccs',uOccs',dOccs',bOccs'} := xSplit(scope', xnet new') .

  eq exploreDn(xst,0) = xst .
  eq exploreDn(xst,s n) = exploreDn(exploreDn1(xst),n)  .

**** Note this works whether or not the occs are in the xnet
  ceq exploreFps(scope,hidden,xnet,uOccs,dOccs,bOccs) =
    xstate(scope3,hidden,xnet new4,new4,sOccs',uOccs',dOccs',bOccs')
  if {scope1,new1} := xnetU(scope,uOccs)
  /\ {scope2,new2} := xnetD(scope1,dOccs)
  /\ {scope3,new3} := xnetB(scope2,bOccs)
  /\ new4 := new1 new2 new3
  /\ {sOccs',uOccs',dOccs',bOccs'} := xSplit(scope3, xnet new4) .

  ceq xsHideRules(scope,hidden,xnet,rids) =
        xstate(scope,hidden new,xnet',new,sOccs,uOccs,dOccs,bOccs)
    if {xnet',new} := splitTrans(xnet,rids,nil) 
    /\ {sOccs,uOccs,dOccs,bOccs} := xSplit(scope, xnet') .

  ceq xsUnHideRules(scope,hidden,xnet,rids) =
        xstate(scope new,hidden',xnet,nil,sOccs,uOccs,dOccs,bOccs)
    if {hidden',new} := splitTrans(hidden,rids,nil) 
    /\ {sOccs,uOccs,dOccs,bOccs} := xSplit(scope new, xnet) .


  op compareXnet : PNTransList PNTransList -> XState .
  ceq compareXnet(pntl0,pntl1) =
      xstate(nil,nil,pntl,nil,allOccs(pntl),none,none,none)
  if pntl := unionTrans(pntl0,pntl1) .

endfm

