
mod RELEVANT-SUBNET is
  inc PETRI .
  inc NAT-QID .

***  op pnTrans : Qid Occs Occs Occs -> PNTrans .
***  op nil : -> PNTransList .
***  op  __ : PNTransList PNTransList -> PNTransList [assoc id: nil] .

  vars pntl pntl' fpntl bpntl : PNTransList .
  var pnt : PNTrans .
  vars ioccs ioccs' ooccs accum unused used goals ngoals ogoals
       omits avoids boccs occs occs' : Occs .
  var rid : Qid .
  var b : Bool .
  var rids rids' : QidList .

  sorts  PNTL3 . **** Transitionlist plus 3 Occ sets
  
  op `{_,_,_,_`} : PNTransList Occs Occs Occs -> PNTL3 [ctor] .

  op pntls-0 : PNTL3 -> PNTransList .
  ops pntls-1 pntls-2 pntls-3 : PNTL3 -> Occs .

  eq pntls-0({pntl,ioccs,unused,used}) = pntl .
  eq pntls-1({pntl,ioccs,unused,used}) = ioccs .
  eq pntls-2({pntl,ioccs,unused,used}) = unused .
  eq pntls-3({pntl,ioccs,unused,used}) = used .

**************************  Ops ***************************************
  op omitRules : PNTransList QidList -> PNTransList .
  op omitRulesX : PNTransList QidList  -> PNTransList .

  op avoidOccs : PNTransList Occs -> PNTransList .
  op avoidOccsX : PNTransList Occs PNTransList -> PNTransList .

****                          Init   
  op fwdCollect : PNTransList Occs -> PNTL3 .
****                    I^Rch I-Rch Rch    *** I-Rch = unused
****       {PNTransList Occs Occs Occs}

****                checking    waiting     collected  accum used more?
  op fwdCollectX : PNTransList PNTransList PNTransList Occs Occs Bool 
                     -> PNTL3 .  **** {fpntl,none,none,used}

****                          Goal                      
  op bwdCollect : PNTransList Occs -> PNTransList .
****                checking    waiting     collected  accum used more?
  op bwdCollectX : PNTransList PNTransList PNTransList Occs Occs Bool 
                     -> PNTransList .

****                         Init Omits
  op prunePNTL : PNTransList Occs Occs ->  PNTL3 .
****                        ioccs goals avoids hides
  op relSubnet : PNTransList Occs Occs Occs QidList -> PNTL3 .
  op relSubnet : PNet Occs Occs QidList -> PNTL3 .
****    {PNTransList Rch I-Rch Rch }

************************** End Ops ***************************************

****  op omitRules : PNTransList QidList  -> PNTransList .
****  op omitRulesX : PNTransList QidList -> PNTransList .
  eq omitRules(pntl,rids) = 
       (if rids == nil
        then pntl
        else omitRulesX(pntl,rids)
        fi) . 

*** cdr through omits
  eq omitRulesX(pntl' pnTrans(rid,ioccs,ooccs,boccs) pntl, rid rids) =
          omitRulesX(pntl' pntl, rids)  .
  eq omitRulesX(pntl, rid rids) = omitRulesX(pntl, rids) [owise] .
  eq omitRulesX(pntl,nil) = pntl .

****  op avoidOccs : PNTransList Occs -> PNTransList .
****  op avoidOccsX : PNTransList Occs PNTransList -> PNTransList .

  eq avoidOccs(pntl,avoids) =
       (if avoids == none
        then pntl
        else avoidOccsX(pntl,avoids,nil) 
        fi) .

  eq avoidOccsX(nil,avoids,pntl) = pntl .
  eq avoidOccsX(pnTrans(rid,ioccs,ooccs,boccs) pntl, avoids, pntl') =
       avoidOccsX(pntl, avoids, pntl'
                 (if Osame(ioccs ooccs boccs,avoids) == none
                  then pnTrans(rid,ioccs,ooccs,boccs)
                  else nil fi)) .

****                              Init   
****  op fwdCollect : PNTransList Occs -> PNTL3 .
****                    Rch  I^Rch I-Rch
****       {PNTransList Occs Occs Occs}

****                   checking    waiting     collected  accum used more?
****  op fwdCollectX : PNTransList PNTransList PNTransList Occs Occs Bool 
****                     -> PNTL3 .  **** {fpntl,accum,used}

  eq fwdCollect(pntl,ioccs) = fwdCol(pntl,ioccs) .

****Alternative for incremental testing

  sort FwdTuple .
  var ft : FwdTuple .
  var n : Nat .
****                    checking   waiting     collected  accum used more?
  op `{_,_,_,_,_,_`} : PNTransList PNTransList PNTransList Occs Occs Bool
         -> FwdTuple .
  ops toCk cked found : FwdTuple -> PNTransList .
  ops accum used : FwdTuple -> Occs .
  op more?  : FwdTuple -> Bool .
  eq toCk({pntl,pntl',fpntl,accum,used,b}) = pntl .
  eq cked({pntl,pntl',fpntl,accum,used,b}) = pntl' .
  eq found({pntl,pntl',fpntl,accum,used,b}) = fpntl .
  eq accum({pntl,pntl',fpntl,accum,used,b}) = accum .
  eq used({pntl,pntl',fpntl,accum,used,b}) = used .
  eq more?({pntl,pntl',fpntl,accum,used,b}) = b .

  op  fwdPass : FwdTuple -> FwdTuple .
 
  op fwdCol : PNTransList Occs -> PNTL3 .
  ceq fwdCol(pntl,ioccs) = 
        {fpntl,Osame(ioccs,used),Odiff(ioccs,used),used} 
      if {nil,pntl',fpntl,accum,used,b} := 
                fwdColX({pntl,nil,nil,ioccs,none,false})  .

  op fwdColX : FwdTuple -> FwdTuple .
  eq fwdColX({nil,pntl',fpntl,accum,used,false}) =
               {nil,pntl',fpntl,accum,used,false} .
      
  eq fwdColX({nil,pntl',fpntl,accum,used,true}) =
       fwdColX({pntl',nil,fpntl,accum,used,false}) .
  
  eq fwdColX({pnt pntl,pntl',fpntl,accum,used,b}) =
       fwdColX(fwdPass({pnt pntl,pntl',fpntl,accum,used,b})) .

****!!!! assume ioccs disjoint boccs
  ceq fwdPass({pnTrans(rid,ioccs,ooccs,boccs) pntl,pntl',fpntl,accum,used,b}) =
       fwdPass({pntl,pntl',fpntl pnTrans(rid,ioccs,ooccs,boccs),
             addOccs(accum,ooccs boccs),
             addOccs(used,ioccs ooccs boccs),
              true})
   if ioccs boccs occs := accum .

   eq fwdPass({pnt pntl,pntl',fpntl,accum,used,b}) =
         fwdPass({pntl,pntl' pnt,fpntl,accum,used,b}) [owise] .

  eq fwdPass({nil,pntl',fpntl,accum,used,b}) = {nil,pntl',fpntl,accum,used,b} .

  op fwdPassX : FwdTuple Nat -> FwdTuple .
  eq fwdPassX(ft,0) = ft .
  ceq fwdPassX(ft,s n) = 
       (if b 
        then fwdPassX({pntl',nil,fpntl,accum,used,b},n)
        else {nil,pntl',fpntl,accum,used,b}
        fi)
     if {nil,pntl',fpntl,accum,used,b} := fwdPass(ft) .


****                            Init Omits
****  op prunePNTL : PNTransList Occs Occs ->  PNTL3 .
  eq prunePNTL(pntl,ioccs,omits) = fwdCollect(pntl,Odiff(ioccs,omits)) .


****                             Goal                      
****  op bwdCollect : PNTransList Occs -> PNTransList .
  
****                  checking    waiting     collected  ngoals ogoals more?
****  op bwdCollectX : PNTransList PNTransList PNTransList Occs Occs Bool 
****                  -> PNTransList .

  eq bwdCollect(pntl,goals) = bwdCollectX(pntl,nil,nil,none,goals,false) .

  eq bwdCollectX(nil,pntl',bpntl,ngoals,ogoals,false) = bpntl .
  eq bwdCollectX(nil,pntl,bpntl,ngoals,ogoals,true) = 
        bwdCollectX(pntl,nil,bpntl,none,ngoals,false) .

  eq bwdCollectX(pnt pntl,pntl',bpntl,ngoals,ogoals,b) =
      (if Osame(pnt2o(pnt),ogoals) =/= none
       then bwdCollectX(pntl,pntl',bpntl pnt,
                        addOccs(ngoals,pnt2pre(pnt)),
                        ogoals,
                        true)
       else bwdCollectX(pntl,pntl' pnt,bpntl,ngoals,ogoals,b) 
       fi) .


****                            ioccs rids  goals avoids
****  op relSubnet : PNTransList Occs Occs Occs QidList-> PNTL3 .
****  op relSubnet : PNet Occs Occs QidList -> PNTL3 .
****!!  omit bwd collect if there are no goals!
  eq relSubnet(pnet(pntl,ioccs),goals,avoids,rids) =
          relSubnet(pntl,ioccs,goals,avoids,rids) .
  ceq relSubnet(pntl,ioccs,goals,avoids,rids) =
              {fpntl,ioccs',unused,used}
  if  pntl' := avoidOccs(omitRules(pntl,rids),avoids)
  /\  bpntl := (if goals == none then pntl' else bwdCollect(pntl',goals) fi)
  /\ {fpntl,ioccs',unused,used} := 
               fwdCollect(bpntl,Odiff(ioccs, avoids)) .


********************* ********************* ********************* 
*****  adding ranks to fwd collection
********************* ********************* ********************* 

**** print QidList as space separated string.  From NAT-ID
****  op qidl2str : QidList -> String .


   sort QidListList .
   op nil : -> QidListList  [ctor] .
   op r : QidList -> QidListList [ctor] .
   op _;_ : QidListList QidListList -> QidListList [ctor assoc id: nil] .
  
   var ql : QidList .
   vars qll ranks : QidListList .
   var str : String .
   var noccs newoccs : Occs .
  
   op qidll2str : QidListList -> String .
   op qidll2strX : QidListList String -> String .
   eq qidll2str(qll) = qidll2strX(qll,"") .
   eq qidll2strX(nil,str) = str .
   eq qidll2strX(r(ql) ; qll, str) 
          = qidll2strX(qll, str + "\n" + qidl2str(ql)) . 


************ 17feb05 clt for rankRule graph annotation
**** would be cleaner to put QidListList elsewhere


   op qidll2arrstr : QidListList -> String .
   op qidll2arrstrX : QidListList String -> String .
   eq qidll2arrstr(qll) = 
         "(array java.lang.Object " + qidll2arrstrX(qll,"") + ")" .
   eq qidll2arrstrX(nil,str) = str .
   eq qidll2arrstrX(r(ql) ; qll, str) 
          = qidll2arrstrX(qll, str + " " + qidl2arrstr(ql)) . 

   op qidl2arrstr : QidList -> String .
   op qidl2arrstrX : QidList String -> String .
   eq qidl2arrstr(ql) = 
         "(array java.lang.String " + qidl2arrstrX(ql,"") + ")" .
   eq qidl2arrstrX(rid ql, str) =
           qidl2arrstrX(ql, str + " " + "\"" + string(rid) + "\"") . 
   eq qidl2arrstrX(nil, str) = str .
 

   sort  PNTL5 . **** Transitionlist plus 3 Occ sets plus rank list
   op `{_,_,_,_,_`} : PNTransList Occs Occs Occs QidListList -> PNTL5 [ctor] .

   sort FwdRTuple .
 ****   checking   waiting   collected  accum used newoccs ranks
   op `{_,_,_,_,_,_,_`} : 
     PNTransList PNTransList PNTransList Occs Occs Occs QidListList 
           -> FwdRTuple .

 
 ****                        Init   
 op fwdCollectRanked : PNTransList Occs -> PNTL5 .
 ****                    Rch  I^Rch I-Rch
 ****       {PNTransList Occs Occs Occs QidListList}

   op fwdPassR : FwdRTuple -> FwdRTuple .

  ceq fwdCollectRanked(pntl,ioccs) = 
        {fpntl,Osame(ioccs,used),Odiff(ioccs,used),used,ranks} 
       if {nil,pntl',fpntl,accum,used,newoccs, ranks } := 
                 fwdPassR({pntl,nil,nil,ioccs,none,none,r(nil)})  .

 ****!!!! assume ioccs disjoint boccs
   ceq fwdPassR({pnTrans(rid,ioccs,ooccs,boccs) pntl,pntl',fpntl,
                accum,used,newoccs, ranks ; r(ql)}) =
        fwdPassR({pntl,pntl',fpntl pnTrans(rid,ioccs,ooccs,boccs),
              accum,
              addOccs(used,ioccs ooccs boccs),
              addOccs(newoccs,ooccs),ranks ; r(ql rid)})
    if ioccs boccs occs := accum .

    eq fwdPassR({pnt pntl,pntl',fpntl,accum,used,newoccs,ranks}) =
          fwdPassR({pntl,pntl' pnt,fpntl,accum,used,newoccs,ranks}) [owise] .

   ceq fwdPassR({nil,pntl',fpntl,accum,used,newoccs,ranks}) =
      (if noccs == none
      then {nil,pntl',fpntl,accum,used,none,ranks}
      else fwdPassR({pntl',nil,fpntl,accum noccs,used,none,ranks ; r(nil)})
      fi ) 
   if noccs := Odiff(newoccs,accum) .
  
 
endm

