******************************************************************************
*** PLA based on IMaude
***  exploring upstream downstream from a focus set incrementally
******************************************************************************
mod PLA-EXPLORE is

  inc RFE .
  inc PLA-AUX .
  inc STATUS-AUX .

  inc META-PETRI .
  inc PNTL2GRAPH .
****  inc GRAPH2G2D .
  inc NEW-GRAPH2G2D .
  inc PLA-GRAPH .
***  inc GRAPH2LOLA .


******************************************************************************
*** Variables
******************************************************************************
var ctl : Control .
var wait4s : Wait4Set .
var reqQ reqQ' reqQ0 reqQ1 reqQ2 : RequestQ .
vars es es' : ESet .
var ee : Entry .
var ee? : Entry? .
var log : Log .

var b b0 bad : Bool .
var n nodeId srcId tgtId : Nat .  var ns : NatList .
vars  mname g2dname g2dvname kbname modname modname' : Qid .
vars type  nid flag qid clab dir nq new? xop replyfor rid : Qid .
vars gname sgname sname pname newgname xgname xname newxname  xkbname : Qid .
vars outQ toks toks' rids history rtoks otoks : QidList .
var ?graph ?graph' graph kbgraph ograph : Graph .
vars pntlT pntlT' sntlT xnetT pnetT occsT ioccsT ioccsT' ooccsT roccsT : Term . 
vars nT ridT occT term : Term .
vars soccsT doccsT uoccsT boccsT : Term .
vars ridsT soccsT' doccsT' uoccsT' boccsT' : Term .
vars scopeT hiddenT newnetT xstateT xstateT' : Term .
vars tl occTL pntTL : TermList .
vars soccTL uoccTL doccTL boccTL : TermList .
vars res0?? res1?? res?? res2?? res3?? : [ResultPair?] .
vars id ?string status str gstr astr rstr title subtitle : String .
vars ctr  ctr1 ctr2  ntype update? occArrStr optArrStr : String .
var val : Val .
vars  gnotes gnotes' pnotes pnotes' xnotes xnotes' notes notes'  : Notes .
vars ndl ndl' nds nodes nodes' ondl ondl' pndl sndl sndl' : NodeList .
vars rnodes inodes onodes bnodes  inodes' onodes' bnodes'  : NodeList .
vars node node' : Node .
var edl oedl oedl' edl' ieds oeds beds : EdgeList .
var mod : Module . 
var bindings : TBinds .
  
******************************************************************************
**** Incremental exploration of net
**** Initiate with gname and initial occs
**** Pnet trans underlying gname is scope for finding rules
**** Could be initiated from tkb or pnet
**** xnet notes include
***(  (("source" := ql(nettype name)),  **** the source of the requesting graph
       ("scopegraph" := gv(scopegname)),
       ("graph" := ql(xgraphname)),  
       ("history" := ql(cmdtoks)),  
       ("scopenet" := tm(modname,pntlT)),  **** current search scope
       ("kbname" := ql(kbname)),  
       ("newnet" := tm(modname,'nil.PNTransList)),  **** increment 
       ("seen" := tm(modname, soccsT) ),   *** processed 
       ("oup" := tm(modname, uoccsT) ),   *** open up only
       ("odn" := tm(modname, doccsT) ),        *** open down only
       ("oboth" := tm(modname, boccsT) ))        *** open up-dn
)

***(graph node attributes
xstatus: oboth (openu and opend)  bluegreen
         oup (openu and seend)  blue
         odn (opend and seenu)  green
         seen (seenu and seend)   gray (lavendar ifinit)
)
******************************************************************************
**** defineXGraph -- as iop graph -
**** if flag == 'false - add new stuff to existing graph
**** ow create from scratch need to know parent graph -- the scopegraph of the xnet
******************************************************************************
  eq isReq('defineXGraph) = true .
****                                     where   what   new?
  eq enabled(wait4s,req('defineXGraph,ql(g2dvname gname flag toks), 
                         reqQ)) = 
      not(waiting4(wait4s,g2dvname)) .

  crl[defineXGraph]:
   [nil,
    st(processing(req('defineXGraph, ql(g2dvname gname flag toks), 
                      reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready,
       (wait4s !
         wait4(g2dvname,gname,
               req('logreq,ql('defineXGraph g2dvname gname flag), 
                    reqQ'))), 
       reqQ,
       es,
       log), outQ 
     g2dvname '\n mname '\n toks' maudePrompt ]
   if gv(?graph) := getVal(es,'gval,gname,gv(mtGraph)) 
   /\ gv(?graph') := lookupd(graphNotes(?graph),"removed",gv(mtGraph))
   /\ gnotes := getNotes(es,'gval,gname)
   /\ ql(kbname) := lookupd(gnotes,"kbname",ql('unknown))
   /\ mname :=  getMaudeName(es)
   /\ ?string :=
        withAck((if (graphNodes(?graph) == nil)
                 then "(apply mtGraphAlert)"
**** 09oct10 to stop the progress bar when no graph is shown
*****            then "(apply displayMessage \"Alert\" \"Empty Graph\")"
                 else (if flag == 'true
                       then mkDefineNewGraphExp(gname,?graph,gnotes)
                       else mkupdXGraphExp(gname,?graph,?graph',gnotes)
****                       else mkdefineXGraphExp(?graph,?graph',gnotes,
****                                               ('kbname 'source), false)
                       fi)
                   fi), mname,g2dvname) 
   /\ toks' := str2toks(?string) .

**** for definition on viewer side
***(       ("gatts" := ql('kbname 'source)),  
           ("oatts" := ql('xinit 'xstatus)),       
           ("ratts" := ql('xinit 'xstatus 'pre 'post)),       
           ("colorFun" := sv("colorXNode")),  
)

******************************************************************************
**** showXGraph -- display an already defined  graph in an explorer frame
******************************************************************************
  eq isReq('showXGraph) = true .
  eq enabled(wait4s,        **** where   parent newg  fresh?
             req('showXGraph,ql(g2dvname pname gname flag toks),reqQ))
        = not(waiting4(wait4s,g2dvname)) .


  crl[showXGraph]:
   [nil,
    st(processing(req('showXGraph,
                      ql(g2dvname pname gname flag toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   (if graphNodes(?graph) == nil
    then [nil,  
          st(ready,wait4s,
             reqQ  
             req('logreq,
                ql('showXGraph 'mtgraph g2dvname pname gname flag toks),
                   reqQ'),
              es, log),
           outQ]
    else [nil,  
          st(ready,
             (wait4s 
               ! wait4(g2dvname,gname,
                req('logreq,
                    ql('showXGraph  g2dvname pname gname flag toks), 
                     reqQ'))), 
              reqQ,
              es,
              log), outQ g2dvname '\n mname '\n toks' maudePrompt ]
    fi)
   if notes := getNotes(es,'gval,gname) 
   /\ gv(?graph) := getVal(es,'gval,gname,gv(mtGraph)) 
   /\ mname :=  getMaudeName(es)
   /\ sv(title) := lookupd(notes,"title",sv(string(gname)))
   /\ sv(subtitle) := lookupd(notes,"subtitle",sv(""))
   /\ ?string := withAck(
                    (if flag == 'true
                     then mkShowNewGraphExp(gname,notes)
                     else mkshowUXGraphExp(gname)
****                     else mkshowXGraphExp(gname,pname,title,subtitle,false)
                     fi),
                    mname,g2dvname) 
   /\ toks' := str2toks(?string) .

******************************************************************************
**** base requests
******************************************************************************
**** initializing
**** sgname -- the requesting/scope graph
**** xname,gname -- names to use for new xnet and its graph
******************************************************************************
  eq isReq('xnetInit) = true .
  eq enabled(wait4s,req('xnetInit,ql(sgname xname gname toks),reqQ)) 
           = true .

  crl[xnetInit]:
   [nil,
    st(processing(req('xnetInit, ql(sgname xname gname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es', log),
    outQ] 
  if {b,es'} := xnetInit(es,sgname,xname,gname)
**** drop contiuation if fails
  /\ reqQ0 :=
      (if b
       then reqQ'
       else  req('logreq,ql('xnetInit 'failed sgname xname gname), nil)
       fi )  .

  op xnetInit : ESet Qid Qid Qid  -> BoolESet .
  ceq xnetInit(es,sgname,xname,gname) = {b,es'}
  if ql(type sname) := 
          lookupd(getNotes(es,'gval,sgname),"source", ql('unknown 'unknown))
  /\ tm(modname,pnetT) := getVal(es,'tval, type sname,dumTv)
  /\ ql(kbname) :=  lookupd(getNotes(es,'gval, sgname),"kbname",ql('unknown))
  /\ b := not(modname == 'BOOL or sname == 'unknown or kbname == 'unknown)
  /\ pntlT := (if b
               then (if getOp(pnetT) == 'pnet 
                     then first(getArgs(pnetT)) 
                     else pnetT fi)
               else 'nil.PNTransList
               fi)
  /\ xnotes := 
     (if not(b) 
     then mt 
     else (("source" := ql(type sname)),   **** source of scopegraph
           ("scopegraph" := ql(sgname)),   
           ("graph" := ql(gname)),      
           ("history" := ql(nil)),
           ("kbname" := ql(kbname)),
           ("scopenet" := tm(modname,pntlT)),
           ("hidden" := tm(modname,'nil.PNTransList)), 
           ("newnet" := tm(modname,'nil.PNTransList)), 
           ("seen" := tm(modname,'none.Occs)),
           ("oup" := tm(modname,'none.Occs)),
           ("odn" := tm(modname,'none.Occs)),
           ("oboth" := tm(modname,'none.Occs)) )
     fi)
  /\ pnotes := getNotes(es,'tval,type sname)
  /\ gnotes :=
     (if not(b) 
     then mt 
     else (("source" := ql('xnet xname)),
           ("requestor" := ql(sgname)),
           ("requestop" := ql('explore)),
           ("requestargs" := sv("")),
           ("kbname" := ql(kbname)),  **** from graph attr of (type sname)
**** for definition on viewer side
           ("gatts" := ql('kbname 'source 
                       'requestor 'requestop 'requestargs)),  
           ("oatts" := ql('xinit 'xstatus)),       
           ("ratts" := ql('xinit 'xstatus 'pre 'post)),       
           ("colorFun" := sv("colorXnetNode")),  
**** for showing
   	     ("title" := 
            sv(mkXGraphTitle(gname, type,
             (if type == 'tkb 
              then sname 
              else getNth(1,qvalQidList(lookupd(pnotes,"dishname",ql(nil))),sname) 
              fi) )) ),
           (if type == 'tkb then mt else ("parent" := ql(sgname)) fi),
           ("subtitle" := sv("")),
           ("selections" := sv("false")),
           ("toolBarFun" := sv("toolBarFunXnet"))
          )  
     fi)                                    
**** ("title" := sv(string(gname) + ": Exploring in " + string(sgname))), 
  /\ es' :=
      (if not(b) 
     then es 
     else addEntry(addEntry(es,
            'tval,'xnet xname,xnotes, tm(modname,'nil.PNTransList)),   
            'gval,gname,gnotes,gv(graph(string(gname),mt,nil,nil)))
     fi)  .

*****************************************************************************
**** forking  -- continue exploring from a copy
**** xname name of the graph being forked
**** newxname newgname -- new names to use for copy
******************************************************************************

  eq isReq('forkX) = true .
  eq enabled(wait4s,req('forkX,ql(xname newxname newgname toks),reqQ)) 
           = true .

 crl[forkX]:
   [nil,
    st(processing(req('forkX, ql(xname newxname newgname toks), 
                      reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es', log),
    outQ]
   if {b,es'} := forkX(es,xname,newxname,newgname)
**** can't continue of fork fails
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('forkX 'failed xname),nil)
       else reqQ'
       fi ) .

  op  forkX : ESet Qid Qid Qid -> BoolESet .
  ceq forkX(es,xname,newxname,newgname) =  {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ xnotes := getNotes(es,'tval,'xnet xname) 
  /\ ql(gname) := lookupd(xnotes,"graph", ql('unknown))
  /\ gv(?graph) := getVal(es,'gval,gname,gv(mtGraph))
  /\ b := not(modname == 'BOOL or gname == 'unknown or ?graph == mtGraph)
  /\ gnotes := getNotes(es,'gval,gname) 
  /\ xnotes' := insert("graph",ql(newgname), xnotes)
  /\ gnotes' := insert("source", ql('xnet newxname),gnotes)
  /\ es' :=
     (if not(b) 
      then es
      else addEntry(addEntry(es,
            'tval,'xnet newxname, xnotes',tm(modname,pntlT)),
            'gval, newgname, gnotes', 
             gv(graph(string(newgname),graphNotes(?graph),
                graphNodes(?graph),graphEdges(?graph))) )
      fi) .


******************************************************************************
**** synching the graph after an exploration operation on the xnet
******************************************************************************

  eq isReq('xgraphSync) = true .
  eq enabled(wait4s,req('xgraphSync,ql(xname flag toks),reqQ)) = true .

 crl[xgraphSync]:
   [nil,
    st(processing(req('xgraphSync, ql(xname flag toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es',log),
    outQ]
   if {b,es'} := xgraphSync(es,xname,flag)
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('xgraphSync 'failed xname flag),
                  nil)
       else reqQ'
       fi ) .

**** the eset update
  op  xgraphSync : ESet Qid Qid -> BoolESet .
  ceq xgraphSync(es,xname,flag) =  {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ xnotes := getNotes(es,'tval,'xnet xname) 
  /\ ql(gname) := lookupd(xnotes,"graph", ql('unknown))
  /\ gv(?graph) := getVal(es,'gval,gname,gv(mtGraph))
  /\ gnotes := getNotes(es,'gval,gname) 
  /\ ql(sgname) := lookupd(xnotes,"scopegraph",ql('unknown))
  /\ sndl := graphNodes(gvalGraph(getVal(es,'gval,sgname,gv(mtGraph))))
  /\ b := not(modname == 'BOOL or gname == 'unknown or ?graph == mtGraph
             or sndl == nil)
  /\ ?graph' := synchXgraph(sndl,?graph,xnotes,flag)
  /\ gnotes' := insert("requestargs", 
                        sv(removeBQs(qidl2str(qvalQidList(
                            lookupd(xnotes,"history",ql(nil)))),0,"")),
                        gnotes)
  /\ es' :=
     (if not(b) 
      then es
      else addEntry(es, 'gval, gname, gnotes', gv(?graph'))
      fi) .

**** set new attribute for old graph, 
**** extend graph, setting new attribute for new elements
**** set xstate attributes for extended graph
  op synchXgraph : NodeList Graph Notes Qid -> Graph .
  ceq synchXgraph(sndl,?graph,xnotes,flag) = 
        graph(graphId(?graph), graphNotes(?graph'),
             setNodesXStatus(graphNodes(?graph'),
                              nil,soccTL,uoccTL,doccTL,boccTL),
             graphEdges(?graph'))
  if tm(modname,pntlT) := lookupd(xnotes,"newnet",dumTv)
  /\ pntTL := (if modname == 'BOOL then empty 
                else olt2tl([modname],'PNTrans,pntlT) fi)
  /\ ndl := setNNotes(graphNodes(?graph),"new",sv("false"),nil)
  /\ edl := setENotes(graphEdges(?graph),"new",sv("false"),nil)
  /\ soccTL := 
       occsT2occTL(tvalTerm(lookupd(xnotes,"seen",tm(modname,'none.Occs))))
  /\ boccTL := 
       occsT2occTL(tvalTerm(lookupd(xnotes,"oboth",tm(modname,'none.Occs))))
  /\ uoccTL := occsT2occTL(tvalTerm(lookupd(xnotes,"oup",tm(modname,'none.Occs))))
  /\ doccTL := occsT2occTL(tvalTerm(lookupd(xnotes,"odn",tm(modname,'none.Occs))))
  /\ ?graph' := 
        (if flag == 'add 
         then extendXGraph(modname,sndl,ndl,edl,nil,nil, pntTL)                                    
         else removeRules(ndl,edl,nil,pntTL)
        fi)  .       

**** these could go into graph.maude
  op setNNotes : NodeList String Val NodeList -> NodeList .
  eq setNNotes(nil,str,val,ndl) = ndl .
  eq setNNotes(nd(nodeId,notes) ndl',str,val,ndl) = 
        setNNotes(ndl',str,val,ndl nd(nodeId,insert(str,val,notes))) .

  op setENotes : EdgeList String Val EdgeList -> EdgeList .
  eq setENotes(nil,str,val,edl) = edl .
  eq setENotes(ed(srcId,tgtId,notes) edl',str,val,edl) = 
        setENotes(edl',str,val,edl ed(srcId,tgtId,insert(str,val,notes))) .

  op extendXGraph : Qid NodeList NodeList EdgeList NodeList EdgeList TermList 
                    -> Graph .
 op extendXGraph1 : Qid  NodeList NodeList EdgeList NodeList EdgeList 
                   NodeList Nat NodeList NodeList NodeList TermList -> Graph .

  eq extendXGraph(modname,sndl,ondl,oedl,ndl,edl,empty) =
           graph("",mt,ondl ndl,oedl edl) .

  eq extendXGraph(modname,sndl,ondl,oedl,ndl,edl, 
                   ('pnTrans[ridT,ioccsT,ooccsT,boccsT],pntTL)) =
     extendXGraph1(modname,sndl,ondl,oedl,ndl,edl,
                   getNodeRidT(sndl,ridT),
                   (if getNodeRidT(sndl,ridT) :: Node 
                    then nodeId(getNodeRidT(sndl,ridT)) else 0 fi),
                   getOccNodes(sndl,occsT2occTL(ioccsT)),
                   getOccNodes(sndl,occsT2occTL(ooccsT)),
                   getOccNodes(sndl,occsT2occTL(boccsT)),
                   pntTL ) .

  eq extendXGraph1(modname,sndl,ondl,oedl,ndl,edl,
                   rnodes,n,inodes,onodes,bnodes,pntTL) = 
     (if rnodes :: Node
      then  extendXGraph(modname,sndl,ondl,oedl,
              addNodes(ndl, setNNotes(rnodes,"new",sv("true"),nil)
                  setNNotes(nodesDiff(inodes,ondl),"new",sv("true"),nil)
                  setNNotes(nodesDiff(onodes,ondl),"new",sv("true"),nil)
                  setNNotes(nodesDiff(bnodes,ondl),"new",sv("true"),nil)),
             (edl
              setENotes(mkIedges(nodes2natl(inodes),n,nil), "new",sv("true"),nil)
              setENotes(mkOedges(nodes2natl(onodes),n,nil), "new",sv("true"),nil)
              setENotes(mkBedges(nodes2natl(bnodes),n,nil), "new",sv("true"),nil)),
            pntTL)
      else  extendXGraph(modname,sndl,ondl,oedl,ndl,edl,pntTL)
      fi) .


  op addNodes : NodeList NodeList -> NodeList .
  eq addNodes(ndl,nil) = ndl .
  eq addNodes(ndl nd(nodeId,notes') ndl', nd(nodeId,notes) ondl) = 
       addNodes(ndl nd(nodeId,notes') ndl', ondl) . 
  eq addNodes(ndl, nd(nodeId,notes) ondl) = 
         addNodes(ndl nd(nodeId,notes), ondl) [owise] . 


  op getOccNodes  : NodeList TermList -> NodeList .
  eq getOccNodes(ndl,empty) = nil .
  eq getOccNodes(ndl nd(nodeId,(notes, ("occ" := tm(modname,occT)))) ndl',
                 (occT, tl)) =
     nd(nodeId,(notes, ("occ" := tm(modname,occT)))) getOccNodes(ndl ndl',tl) .
  eq getOccNodes(ndl,(occT,tl)) = getOccNodes(ndl,tl) [owise] .

  op nodesDiff : NodeList NodeList  -> NodeList .
  eq nodesDiff(nil, ndl) = nil .
  eq nodesDiff(nd(nodeId,notes) ndl', ondl) =
      (if getNode(ondl,nodeId) :: Node then nil else nd(nodeId,notes) fi)
       nodesDiff(ndl',ondl) .


  op getNodeRidT : NodeList Term -> NodeList .
  eq getNodeRidT(sndl nd(nodeId,(notes, ("rule" := tm(modname,ridT)))) sndl',
                 ridT)
     = nd(nodeId,(notes, ("rule" := tm(modname,ridT)))) .
  eq getNodeRidT(sndl,ridT) = nil [owise] .

****                seenu seend openu opend occ
  op occs2xstatus : TermList TermList  TermList  TermList  Term -> String .
  eq occs2xstatus(soccTL,uoccTL,doccTL,boccTL,occT) =
       (if eltOf(occT,soccTL)
        then "seen"
        else (if eltOf(occT,uoccTL) then "oup"
        else (if eltOf(occT,doccTL) then "odn" else "oboth" fi) fi) fi) .

  op setNodesXStatus : NodeList NodeList TermList TermList TermList TermList
                       -> NodeList .
  eq setNodesXStatus(nil,ndl,soccTL,uoccTL,doccTL,boccTL) = ndl .
  eq setNodesXStatus(nd(nodeId,notes) ndl',ndl,soccTL,uoccTL,doccTL,boccTL) =
      setNodesXStatus(ndl',ndl nd(nodeId, 
                      setNotesXStatus(notes,soccTL,uoccTL,doccTL,boccTL)),
                      soccTL,uoccTL,doccTL,boccTL) .

  op setNotesXStatus : Notes TermList TermList TermList TermList -> Notes .
  eq setNotesXStatus(notes,soccTL,uoccTL,doccTL,boccTL) =
       (if lookupd(notes,"type",sv("")) == sv("occ")
        then insert("xstatus",
                    sv(occs2xstatus(soccTL,uoccTL,doccTL,boccTL,
                       tvalTerm(lookupd(notes,"occ",dumTv)))),
                    notes)
        else notes
        fi) .


****               remain   orig     removed toremove 
  op removeRules : NodeList EdgeList NodeList TermList  -> Graph .
****               remain   remain   tock      cked     removed
  op removeEdges : NodeList EdgeList NodeList NodeList EdgeList  -> Graph .
****               tock    keep     remain   removed  removed
  op removeOccs : NodeList NodeList EdgeList NodeList EdgeList  -> Graph .


  eq removeRules(ondl,oedl,ndl,empty) = removeEdges(ondl,oedl,ndl,nil,nil) .
  eq removeRules(ondl nd(nodeId,(notes,("rule" := tm(modname,ridT)))) ondl', 
                 oedl,ndl,('pnTrans[ridT,ioccsT,ooccsT,boccsT],pntTL)) =
      removeRules(ondl ondl',oedl, 
                  ndl nd(nodeId,(notes, ("rule" := tm(modname,ridT)))),
                  pntTL) .
**** shouldn't happen ... but
  eq removeRules(ondl,oedl,ndl,('pnTrans[ridT,ioccsT,ooccsT,boccsT],pntTL)) =
       removeRules(ondl,oedl,ndl,pntTL) [owise] .

****    remaining nds,eds,tock cked removed
  eq removeEdges(ondl,oedl,nil,ndl,edl) = removeOccs(ondl,nil,oedl,ndl,edl) .

  eq removeEdges(ondl,oedl ed(nodeId,tgtId,notes') oedl',
                 nd(nodeId,notes) ndl,ndl',edl)  =
       removeEdges(ondl,oedl oedl', nd(nodeId,notes) ndl,ndl', 
                   edl ed(nodeId,tgtId,notes')) .
  eq removeEdges(ondl,oedl ed(srcId,nodeId,notes') oedl',
                 nd(nodeId,notes) ndl,ndl',edl)  =
       removeEdges(ondl,oedl oedl', nd(nodeId,notes) ndl,ndl', 
                   edl ed(srcId,nodeId,notes')) .
  eq removeEdges(ondl,oedl', nd(nodeId,notes) ndl,ndl',edl)  =
        removeEdges(ondl,oedl',ndl,ndl' nd(nodeId,notes) ,edl)  [owise] .

****         tock   keep keep rmv rmv
  eq removeOccs(nil,ondl,oedl,ndl,edl) =
      graph("", ("removed" := gv(graph("",mt,ndl,edl))),ondl,oedl) .

  eq removeOccs(nd(nodeId,notes) ondl,ondl',
                oedl ed(srcId,nodeId,notes') oedl',ndl,edl) =
       removeOccs(ondl,ondl' nd(nodeId,notes),
                  oedl ed(srcId,nodeId,notes') oedl',ndl,edl) .
  eq removeOccs(nd(nodeId,notes) ondl,ondl',
                oedl ed(nodeId,tgtId,notes') oedl',ndl,edl) =
       removeOccs(ondl,ondl' nd(nodeId,notes),
                  oedl ed(nodeId,tgtId,notes') oedl',ndl,edl) .
  eq removeOccs(nd(nodeId,notes) ondl,ondl',oedl,ndl,edl) =
       removeOccs(ondl,ondl', oedl, ndl nd(nodeId,notes),edl) [owise] .



***************************************************************************
**** manipulating xstate terms

***************************************************************************
  op mtXstateT : -> Term .
  eq mtXstateT = 'xstate['nil.PNTransList,'nil.PNTransList,
                         'nil.PNTransList,'nil.PNTransList,
                         'none.Occs,'none.Occs,'none.Occs,'none.Occs] .

  ops xstateT2scopeT xstateT2xnetT xstateT2newnetT  xstateT2hiddenT
      : Term -> Term .
  ops xstateT2soccsT xstateT2uoccsT xstateT2doccsT xstateT2boccsT
      : Term -> Term .

  eq xstateT2scopeT('xstate[scopeT,hiddenT,xnetT,newnetT,
                            soccsT,uoccsT,doccsT,boccsT]) = scopeT . 
  eq xstateT2scopeT(term) = 'nil.PNTransList [owise] .

  eq xstateT2xnetT('xstate[scopeT,hiddenT,xnetT,newnetT,
                           soccsT,uoccsT,doccsT,boccsT]) = xnetT . 
  eq xstateT2xnetT(term) = 'nil.PNTransList [owise] .

  eq xstateT2newnetT('xstate[scopeT,hiddenT,xnetT,newnetT,
                             soccsT,uoccsT,doccsT,boccsT]) = newnetT . 
  eq xstateT2newnetT(term) = 'nil.PNTransList [owise] .

  eq xstateT2hiddenT('xstate[scopeT,hiddenT,xnetT,newnetT,
                             soccsT,uoccsT,doccsT,boccsT]) = hiddenT . 
  eq xstateT2hiddenT(term) = 'nil.PNTransList [owise] .

  eq xstateT2soccsT('xstate[scopeT,hiddenT,xnetT,newnetT,
                            soccsT,uoccsT,doccsT,boccsT]) = soccsT . 
  eq xstateT2soccsT(term) = 'none.Occs [owise] .

  eq xstateT2uoccsT('xstate[scopeT,hiddenT,xnetT,newnetT,
                            soccsT,uoccsT,doccsT,boccsT]) = uoccsT . 
  eq xstateT2uoccsT(term) = 'none.Occs [owise] .

  eq xstateT2doccsT('xstate[scopeT,hiddenT,xnetT,newnetT,
                            soccsT,uoccsT,doccsT,boccsT]) = doccsT . 
  eq xstateT2doccsT(term) = 'none.Occs [owise] .

  eq xstateT2boccsT('xstate[scopeT,hiddenT,xnetT,newnetT,
                            soccsT,uoccsT,doccsT,boccsT]) = boccsT . 
  eq xstateT2boccsT(term) = 'none.Occs [owise] .


  op updateXnotes : Notes Qid Term QidList -> Notes .
  eq updateXnotes(xnotes,modname,xstateT,toks) =
          (("source" := lookupd(xnotes,"source",ql('unknown 'unknown))),
           ("scopegraph" := lookupd(xnotes,"scopegraph",ql('unknown))),
           ("graph" := lookupd(xnotes,"graph",ql('unknown))),
           ("kbname" := lookupd(xnotes,"kbname",ql('unknown))),
           ("history" :=
                 ql(qvalQidList(lookupd(xnotes,"history",ql(nil))) toks)),
           ("scopenet" := tm(modname,xstateT2scopeT(xstateT))),
           ("hidden" := tm(modname,xstateT2hiddenT(xstateT))), 
           ("newnet" := tm(modname,xstateT2newnetT(xstateT))), 
           ("seen" := tm(modname,xstateT2soccsT(xstateT))),
           ("oup" := tm(modname,xstateT2uoccsT(xstateT))),
           ("odn" := tm(modname,xstateT2doccsT(xstateT))),
           ("oboth" := tm(modname,xstateT2boccsT(xstateT))) ) .


******************************************************************************
*** adding rules
******************************************************************************

  eq isReq('xaddRules) = true .
  eq enabled(wait4s,req('xaddRules,ql(xname toks),reqQ)) 
           = true .

 crl[xaddRules]:
   [nil,
    st(processing(req('xaddRules, ql(xname toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es', log),
    outQ]
   if {b,es'} := xaddRules(es,xname,toks)
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('xaddRules 'failed xname toks),nil)
       else req('xgraphSync,ql(xname 'add),reqQ')
       fi ) .


  op xaddRules : ESet Qid QidList -> BoolESet .
  ceq xaddRules(es,xname,rids) = {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ ridsT := qidl2qidlT(rids)
  /\ xnotes := getNotes(es,'tval,'xnet xname)
  /\ scopeT := tvalTerm(lookupd(xnotes,"scopenet",dumTv))
  /\ hiddenT := tvalTerm(lookupd(xnotes,"hidden",dumTv))
  /\ res?? := metaReduce([modname],'xsAddRules[scopeT,hiddenT,pntlT,ridsT])
  /\ b :=  modname =/= 'BOOL or res?? :: ResultPair
  /\ xstateT := (if b then getTerm(res??) else mtXstateT fi) 
  /\ ql(history) := lookupd(xnotes,"history",ql(nil))
  /\ xnotes' := 
      (if not(b)
       then mt
       else updateXnotes(xnotes,modname,xstateT,'`( 'addR rids '`))
       fi)
  /\ es' := 
      (if not(b)
       then es
       else addEntry(es,'tval,'xnet xname, 
                         xnotes',tm(modname,xstateT2xnetT(xstateT)))
       fi) .

******************************************************************************
*** hiding rules
******************************************************************************
  eq isReq('xhideRules) = true .
  eq enabled(wait4s,req('xhideRules,ql(xname toks),reqQ)) = true .

 crl[xhideRules]:
   [nil,
    st(processing(req('xhideRules, ql(xname toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es', log),
    outQ]
   if {b,es'} := xhideRules(es,xname,toks)
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('xhideRules 'failed xname toks),nil)
       else req('xgraphSync,ql(xname 'remove),reqQ')
       fi ) .

  op xhideRules : ESet Qid QidList -> BoolESet .
  ceq xhideRules(es,xname,rids) = {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ ridsT := qidl2qidlT(rids)
  /\ xnotes := getNotes(es,'tval,'xnet xname)
  /\ scopeT := tvalTerm(lookupd(xnotes,"scopenet",dumTv))
  /\ hiddenT := tvalTerm(lookupd(xnotes,"hidden",dumTv))
  /\ res?? := metaReduce([modname],'xsHideRules[scopeT,hiddenT,pntlT,ridsT])
  /\ b :=  modname =/= 'BOOL or res?? :: ResultPair
  /\ xstateT := (if b then getTerm(res??) else mtXstateT fi) 
  /\ xnotes' := 
      (if not(b)
       then mt
       else updateXnotes(xnotes,modname,xstateT,'`( 'hideR rids '`) )
       fi)
  /\ es' := 
      (if not(b)
       then es
       else addEntry(es,'tval,'xnet xname, 
                         xnotes',tm(modname,xstateT2xnetT(xstateT)))
       fi) .

******************************************************************************
*** unhiding rules
******************************************************************************
  eq isReq('xunhideRules) = true .
  eq enabled(wait4s,req('xunhideRules,ql(xname toks),reqQ)) = true .

 crl[xhideRules]:
   [nil,
    st(processing(req('xunhideRules, ql(xname toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es', log),
    outQ]
   if {b,es'} := xunhideRules(es,xname,toks)
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('xunhideRules 'failed xname toks),nil)
       else req('xgraphSync,ql(xname 'add),reqQ') 
****   else reqQ'   **** the xnet hasn't changed, but graph colors might
       fi ) .

  op xunhideRules : ESet Qid QidList -> BoolESet .
  ceq xunhideRules(es,xname,rids) = {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ ridsT := qidl2qidlT(rids)
  /\ xnotes := getNotes(es,'tval,'xnet xname)
  /\ scopeT := tvalTerm(lookupd(xnotes,"scopenet",dumTv))
  /\ hiddenT := tvalTerm(lookupd(xnotes,"hidden",dumTv))
  /\ res?? := metaReduce([modname],'xsUnHideRules[scopeT,hiddenT,pntlT,ridsT])
  /\ b :=  modname =/= 'BOOL or res?? :: ResultPair
  /\ xstateT := (if b then getTerm(res??) else mtXstateT fi) 
  /\ xnotes' := 
      (if not(b)
       then mt
       else updateXnotes(xnotes,modname,xstateT,'`( 'unhideR rids '`) )
       fi)
  /\ es' := 
      (if not(b)
       then es
       else addEntry(es,'tval,'xnet xname, 
                         xnotes',tm(modname,xstateT2xnetT(xstateT)))
       fi) .


******************************************************************************
*** explore from focus points
******************************************************************************

  eq isReq('xnetFps) = true .
  eq enabled(wait4s,req('xnetFps,ql(xname toks),reqQ)) = true .

 crl[xnetFps]:
   [nil,
    st(processing(req('xnetFps, ql(xname toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil, st(ready, wait4s, reqQ reqQ0, es', log), outQ]
   if {b,es'} := xnetFps(es,xname,toks)
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('xnetFps 'failed xname toks),nil)
       else req('xgraphSync,ql(xname 'add),reqQ')
       fi ) .

  op xnetFps : ESet Qid QidList -> BoolESet .
  ceq xnetFps(es,xname,toks) = {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ xnotes := getNotes(es,'tval,'xnet xname)
  /\ scopeT := tvalTerm(lookupd(xnotes,"scopenet",dumTv))
  /\ hiddenT := tvalTerm(lookupd(xnotes,"hidden",dumTv))
  /\ ql(sgname) := lookupd(xnotes,"scopegraph",ql('unknown))
  /\ gv(?graph) := getVal(es,'gval,sgname,gv(mtGraph))
  /\ (uoccsT,doccsT,boccsT) :=
            parseFpsToks(graphNodes(?graph),toks,empty,empty,empty)
  /\ res?? := metaReduce([modname],
                        'exploreFps[scopeT,hiddenT,pntlT,uoccsT,doccsT,boccsT])
  /\ b :=  modname =/= 'BOOL or res?? :: ResultPair
  /\ xstateT := (if b then getTerm(res??) else mtXstateT fi) 
  /\ xnotes' := 
      (if not(b)
       then mt
       else updateXnotes(xnotes,modname,xstateT, '`( 'fps  toks '`))
       fi)
  /\ es' := 
      (if not(b)
       then es
       else addEntry(es,'tval,'xnet xname, 
                         xnotes',tm(modname,xstateT2xnetT(xstateT)))
       fi) .

  op parseFpsToks : NodeList QidList TermList TermList TermList -> TermList .
  ceq parseFpsToks(ndl,qid dir toks,uoccTL,doccTL,boccTL) =
       (if modname == 'BOOL
        then parseFpsToks(ndl,toks,uoccTL,doccTL,boccTL)
        else (if dir == 'u
              then parseFpsToks(ndl,toks,(uoccTL,occT),doccTL,boccTL)
              else (if dir == 'd
      		  then parseFpsToks(ndl,toks,uoccTL,(doccTL,occT),boccTL)
			     else (if dir == 'b
			     then parseFpsToks(ndl,toks,uoccTL,doccTL,(boccTL,occT))
			     else parseFpsToks(ndl,toks,uoccTL,doccTL,boccTL)
			     fi) fi) fi)
       fi)
  if nodes := getNode(ndl,"chattylabel",sv(string(qid)))
  /\ tm(modname,occT) :=
       (if nodes :: Node 
        then lookupd(nodeNotes(nodes),"occ",dumTv)
        else dumTv fi) .

  eq parseFpsToks(ndl, toks,uoccTL,doccTL,boccTL) =
      (occTL2occsT(uoccTL),occTL2occsT(doccTL),occTL2occsT(boccTL))  [owise] .


******************************************************************************
*** going up/down
******************************************************************************
  eq isReq('xnetUpDn) = true .
  eq enabled(wait4s,req('xnetUpDn,ql(xname dir nq toks),reqQ)) 
           = true .

 crl[xnetUpDn]:
   [nil,
    st(processing(req('xnetUpDn, ql(xname dir nq toks), reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, es', log),
    outQ]
   if {b,es'} := xnetUpDn(es,xname,dir,nq)
   /\ reqQ0 :=
      (if not(b)
       then req('logreq,ql('xnetUpDn 'failed xname dir nq toks),nil)
       else req('xgraphSync,ql(xname 'add),reqQ')
       fi ) .


  op xnetUpDn : ESet Qid Qid Qid -> BoolESet .
  ceq xnetUpDn(es,xname,dir,nq) = {b,es'}
  if tm(modname,pntlT) := getVal(es,'tval,'xnet xname,dumTv)
  /\ nT := nat2natT(if rat(string(nq),10) :: Nat
                     then rat(string(nq),10) 
                     else 0 fi)
  /\ xnotes := getNotes(es,'tval,'xnet xname)
  /\ scopeT := tvalTerm(lookupd(xnotes,"scopenet",dumTv))
  /\ hiddenT := tvalTerm(lookupd(xnotes,"hidden",dumTv))
  /\ newnetT := tvalTerm(lookupd(xnotes,"newnet",dumTv))
  /\ soccsT := tvalTerm(lookupd(xnotes,"seen",dumTv))
  /\ uoccsT := tvalTerm(lookupd(xnotes,"oup",dumTv))
  /\ doccsT := tvalTerm(lookupd(xnotes,"odn",dumTv))
  /\ boccsT := tvalTerm(lookupd(xnotes,"oboth",dumTv))
  /\ xstateT' := 'xstate[scopeT,hiddenT,pntlT,newnetT,soccsT,uoccsT,doccsT,boccsT]
  /\ bad :=  modname == 'BOOL or 
     eltOf('true.Bool, (scopeT, newnetT, hiddenT, soccsT, uoccsT, doccsT, boccsT))
  /\ res?? := 
      (if bad then noParse(0) else
      (if dir == 'up
       then metaReduce([modname],'exploreUp[xstateT',nT])
       else (if dir == 'dn
       then metaReduce([modname],'exploreDn[xstateT',nT])
       else noParse(0) fi) fi)  fi) ****HACK 
  /\ b :=  not(bad) and res?? :: ResultPair
  /\ xstateT := (if b
                 then getTerm(res??)
                 else mtXstateT fi) 
  /\ xnotes' := 
      (if not(b)
       then mt
       else updateXnotes(xnotes,modname,xstateT,'`( dir nq '`))
     fi)
  /\ es' := 
      (if not(b)
       then es
       else addEntry(es,'tval,'xnet xname, 
                         xnotes',tm(modname,xstateT2xnetT(xstateT)))
       fi) .

******************************************************************************
**** posting explore dialogs
**** req('exploreSelect, ql(g2dvname sgname xgname new? op),
****     req(<xnetopreq>, ql(xname),reqQ2))
****  From exploreInit sgname will be the caller, xgname the new graph name
****    new?  will be true and op will be one of 'fps or 'addR
****  From explore sgname will be the scopegraph of the caller
****    xgname the graph of the net to edit, 
****    op is one of  of 'fps or 'addR or 'hideR
****    of new? is 'true the xgname the copy of the caller ow the caller
****    in the case of hideRules the scope is xgname
****  If explore string is "" and new? is not 'true then restart xname listener
****  send viewer the code to open the selection dialog
****  with continuation that bails if there is a dismiss
****  and strips the request id from toks before supplying them to the cont
************************************************************************
  eq isReq('exploreSelect) = true .
****                                     viewer   scope     rules or occs
  eq enabled(wait4s,req('exploreSelect,
                         ql(g2dvname sgname xgname  new? xop toks),reqQ)) 
           = true .
 crl[exploreSelect]:
   [nil,
    st(processing(req('exploreSelect,
                       ql(g2dvname sgname xgname  new? xop toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, 
       (if ?string == ""
        then wait4s 
        else wait4s ! wait4(replyfor, 'exploreSelect xgname xop,
                              req('exploreSelectReply,ql(nil), reqQ'))
        fi), 
       (reqQ reqQ0), incGlobalCounter(es,1), log), 
    outQ toks']
   if mname :=  getMaudeName(es)
   /\ ql(type xname) :=
          lookupd(getNotes(es,'gval,xgname),"source",ql('unknown 'unknown))
   /\ xnotes := getNotes(es,'tval,type xname)
   /\ tm(modname,pntlT) :=
      (if xop == 'hideR 
       then getVal(es,'tval,type xname,dumTv)
       else (if xop == 'addR 
             then lookupd(xnotes,"scopenet",dumTv)
             else (if xop == 'unhideR 
                   then  lookupd(xnotes,"hidden",dumTv)
                   else dumTv fi)
             fi)
       fi)
   /\ pntTL := (if modname == 'BOOL then empty 
                else olt2tl([modname],'PNTrans,pntlT) fi)
   /\ sndl := graphNodes(gvalGraph(getVal(es,'gval,sgname,gv(mtGraph))))
   /\ replyfor := qid("maudereq" + getGlobalCounter(es))
   /\ title := 
       (if xop == 'fps
        then "Select occs and direction to explore from " + string(xgname)
        else (if xop == 'addR
        then "Select rules to add to " + string(xgname)
        else (if xop == 'hideR
        then "Select rules to hide from " + string(xgname)
        else (if xop == 'unhideR
        then "Select rules to unhide from " + string(xgname)
        else "" fi) fi) fi) fi)
   /\ gname := (if new? == 'true then sgname else xgname fi)
   /\  ?string :=
        (if xname == 'unknown
         then ""
         else (if xop == 'fps
              then exploreSelectOccsString(title,gname,mname,replyfor,
                                           sndl)
              else exploreSelectRulesString(title,gname,mname,replyfor,pntTL)
              fi)
         fi)
   /\ toks' := (if ?string == "" 
                then nil 
                else g2dvname '\n mname '\n str2toks(?string) maudePrompt
                fi)
   /\ reqQ0 :=
      (if ?string == ""  *** drop the select continuation as it has no input
       then req('logreq,ql('exploreSelect 'failed g2dvname sgname xgname toks),
             req('sendAlert, 
                 ql(g2dvname 'exploreSelect sgname xgname 'failed), 
               (if new? == 'true 
                then nil
                else req('startcListener,ql(xgname 'serializingListener g2dvname),
                   nil) fi)))
       else nil
      fi) .


**** exploreInit will popup selector, send selection to replyto from replyfor
****  expects replyfor to be listening
  op exploreSelectRulesTemplate : -> String .
  eq exploreSelectRulesTemplate = 
      "(apply exploreSelectRules %title %gname %rids %replyto %replyfor)" .
  op exploreSelectOccsTemplate : -> String .
  eq exploreSelectOccsTemplate = 
      "(apply exploreSelectOccs %title %gname %occids %replyto %replyfor)" .

  op exploreSelectRulesString : String Qid Qid Qid  TermList  -> String .
  ceq exploreSelectRulesString(title,gname,mname,replyfor,pntTL) =
        fillTemplate(exploreSelectRulesTemplate,bindings)
  if bindings :=              
       (("%title" :~ squote(title)),
        ("%gname" :~ squote(string(gname))),
        ("%rids" :~ 
            "(array java.lang.String " + mkRidStr(pntTL,"") + ")" ),
        ("%replyto" :~ squote(string(mname))),
        ("%replyfor" :~ squote(string(replyfor)))) .

  ops mkRidStr : TermList String -> String .
  eq mkRidStr(('pnTrans[ridT,ioccsT,ooccsT,boccsT], tl),str) = 
        mkRidStr(tl,str + " " + squote(printRidTAll(ridT))) . 
  eq mkRidStr(empty,str) = str .

  op exploreSelectOccsString : String Qid Qid Qid NodeList -> String .
****                           title   gn  mn  for sndl

  ceq exploreSelectOccsString(title,gname,mname,replyfor,sndl) =
        fillTemplate(exploreSelectOccsTemplate,bindings)
   if bindings :=              
       (("%title" :~ squote(title)),
        ("%gname" :~ squote(string(gname))),
        ("%occids" :~ "(array java.lang.String " + ndl2occstr(sndl,"") + ")" ),
        ("%replyto" :~ squote(string(mname))),
        ("%replyfor" :~ squote(string(replyfor)))) .
  

  op ndl2occstr : NodeList String -> String .
  eq ndl2occstr(nil,str) = str .
  eq ndl2occstr(nd(nodeId,notes) sndl,str) = 
      ndl2occstr(sndl,  
                  (if lookupd(notes,"type",sv("")) == sv("occ")
                  then str + " " + 
                        squote(svalString(lookupd(notes,"chattylabel",sv("")))) 
                  else str fi)) .

************************************************************************
****  forwarding selection from dialog
****  drop req cont if toks == nil -- selector dismissed
****                                  scope viewer   rule or occ 
  eq enabled(wait4s, req('exploreSelectReply,ql(replyfor toks),reqQ)) 
           = true .
 rl[exploreSelectReply]:
   [nil,
    st(processing(req('exploreSelectReply, 
                      ql(replyfor toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, 
       (if toks == nil 
        then req('sendAlert,
                 ql(getG2dVName(es) 'exploreSelect 'empty 'selection), reqQ) 
        else reqQ supplyPars(reqQ',toks) fi),
**** reqQ (if toks == nil then nil else supplyPars(reqQ',toks) fi),
       es, log),
    outQ] .


******************************************************************************
**** Viewer Interface
**** exploreInit
**** explore
************************************************************************
  eq isReq('exploreInit) = true .
****                          from/scope viewer  rule or occ 
  eq enabled(wait4s,
             req('exploreInit,ql(gname g2dvname flag  toks),reqQ)) 
           = true .
 crl[exploreInit]:
   [nil,
    st(processing(req('exploreInit, 
                      ql(gname g2dvname flag toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, incGlobalCounter(es,2), log),
    outQ]
   if ctr := getGlobalCounter(es) 
   /\ ctr1 := stringInc(ctr) 
   /\ xname := qid("xpnet" + ctr)
   /\ newgname := qid("graph" + ctr1)
   /\ reqQ2 := 
        req('defineXGraph,ql(g2dvname newgname 'true),
           req('showXGraph,ql(g2dvname gname newgname 'true),
             req('startcListener,ql(newgname 'serializingListener g2dvname),
                reqQ')))
   /\ reqQ1 :=
        (if flag == 'rule
         then  req('exploreSelect, ql(g2dvname gname newgname 'true 'addR),
                    req('xaddRules,ql(xname toks),reqQ2))
         else (if flag == 'occ 
              then req('exploreSelect, ql(g2dvname gname newgname 'true 'fps),
                     req('xnetFps,ql(xname toks),reqQ2))
              else reqQ2 fi) fi)
   /\ reqQ0 :=
      (if  (flag =/= 'occ and flag =/= 'rule)
       then req('logreq,ql('exploreInit 'failed gname  g2dvname  flag),reqQ')
       else req('xnetInit,ql(gname xname newgname),reqQ1)
      fi) .

************************************************************************
**** 10jan30 -- hack to show maude rule as pnet -- which can be explored
************************************************************************
  eq isReq('exploreRule) = true .
****                          from/scope viewer  rule or occ 
  eq enabled(wait4s,
             req('exploreRule,ql(gname g2dvname rid  toks),reqQ)) 
           = true .
 crl[exploreRule]:
   [nil,
    st(processing(req('exploreRule, 
                      ql(gname g2dvname rid toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, incGlobalCounter(es,2), log),
    outQ]
   if ctr := getGlobalCounter(es) 
   /\ ctr1 := stringInc(ctr) 
   /\ xname := qid("xpnet" + ctr)
   /\ newgname := qid("graph" + ctr1)
   /\ reqQ2 := 
        req('defineXGraph,ql(g2dvname newgname 'true),
           req('showXGraph,ql(g2dvname gname newgname 'true),
             req('startcListener,ql(newgname 'serializingListener g2dvname),
                reqQ')))
   /\ reqQ0 := req('xnetInit,ql(gname xname newgname),
                   req('xaddRules,ql(xname rid toks),reqQ2))
  .


************************************************************************
**** 13aug24 -- initiate occ exploration from context menu
************************************************************************
  eq isReq('exploreOcc) = true .
****                          from/scope viewer  rule or occ 
  eq enabled(wait4s,
             req('exploreOcc,ql(gname g2dvname clab dir toks),reqQ)) 
           = true .
 crl[exploreOcc]:
   [nil,
    st(processing(req('exploreOcc, 
                      ql(gname g2dvname clab dir toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s, reqQ reqQ0, incGlobalCounter(es,2), log),
    outQ]
   if ctr := getGlobalCounter(es) 
   /\ ctr1 := stringInc(ctr) 
   /\ xname := qid("xpnet" + ctr)
   /\ newgname := qid("graph" + ctr1)
   /\ reqQ2 := 
        req('defineXGraph,ql(g2dvname newgname 'true),
           req('showXGraph,ql(g2dvname gname newgname 'true),
             req('startcListener,ql(newgname 'serializingListener g2dvname),
                reqQ')))
   /\ reqQ0 := req('xnetInit,ql(gname xname newgname),
                   req('xnetFps,ql(xname clab  dir toks),reqQ2))
  .

***************************************************************************
**** exploring
**** flag == 'true then  fork else use existing xnet/graph
****  if xname or sgname == 'unknown then fail, don't restart xgname
****  if op not understood, explore fails but restart xgname 
**** if new restart xgname after forkX ow will be restarted after showX
***************************************************************************
  eq isReq('explore) = true .
****                                from    viewer            [n]
  eq enabled(wait4s,req('explore,ql(xgname  g2dvname new? xop toks),reqQ)) 
           = true .

 crl[explore]:
   [nil,
    st(processing(req('explore, ql(xgname g2dvname new? xop toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready,
****       (if new? == 'true 
****        then wait4s ! 
****             wait4(xgname, nil, creq('onetimeListener,nil,ql(g2dvname),nil))
****        else wait4s fi),
       wait4s,
       reqQ reqQ0, 
       (if new? == 'true then incGlobalCounter(es,2) else es fi),
       log),
    outQ]
**** type should be 'xnet
  if ql(type xname) :=
       lookupd(getNotes(es,'gval,xgname),"source",ql('unknown 'unknown))
  /\ ql(sgname) := lookupd(getNotes(es,'tval, type xname), 
                         "scopegraph", ql('unknown) )
  /\ newxname := 
       (if new? == 'true 
        then qid("xpnet" + getGlobalCounter(es)) else xname fi)
  /\ newgname :=
       (if new? == 'true 
        then qid("graph" + stringInc(getGlobalCounter(es))) else xgname fi)
  /\ nodes := graphNodes(gvalGraph(getVal(es,'gval,xgname,gv(mtGraph))))
  /\ rtoks := getRuleToks(nodes,toks)
  /\ otoks := getOccToks(nodes,toks)
  /\ reqQ2 :=
       req('defineXGraph,ql(g2dvname newgname new?),
         req('showXGraph,ql(g2dvname sgname newgname new?),
           req('startcListener,ql(newgname 'serializingListener g2dvname),reqQ')))
  /\ reqQ1 := 
    (if (xop == 'up or xop == 'dn )
     then req('xnetUpDn, ql(newxname xop toks),reqQ2)
     else (if (xop == 'selected)
     then (if rtoks == nil
           then req('xnetFps,ql(newxname otoks),reqQ2)
           else (if otoks == nil
           then req('xhideRules,ql(newxname rtoks),reqQ2)
           else req('xhideRules,ql(newxname rtoks),
                  req('defineXGraph,ql(g2dvname newgname new?),
                    req('xnetFps,ql(newxname otoks),
                     req('defineXGraph,ql(g2dvname newgname 'false),
                      req('showXGraph,ql(g2dvname sgname newgname 'false),
                        req('startcListener,
                            ql(newgname 'serializingListener g2dvname),reqQ'))))))
               fi) fi) 
     else  (if xop == 'fps 
     then req('exploreSelect, ql(g2dvname sgname xgname new? xop),
              req('xnetFps, ql(newxname),reqQ2))
     else (if xop == 'addR 
     then  req('exploreSelect, ql(g2dvname sgname xgname new? xop),
               req('xaddRules, ql(newxname),reqQ2))
     else (if xop == 'hideR 
     then  req('exploreSelect, ql(g2dvname xgname xgname new? xop),
               req('xhideRules, ql(newxname),reqQ2))
     else (if xop == 'unhideR 
     then  req('exploreSelect, ql(g2dvname xgname xgname new? xop),
               req('xunhideRules, ql(newxname),reqQ2))
     else req('logreq,ql('explore 'failed  g2dvname xgname new? xop toks),
              req('startcListener,ql(xgname 'serializingListener g2dvname), 
                  reqQ'))
     fi) fi) fi) fi) fi) fi)
  /\ reqQ0 :=
       (if xname == 'unknown or sgname == 'unknown
        then req('logreq,ql('explore 'failed xgname g2dvname new? xop toks), 
                 reqQ')
        else (if new? == 'true
               then req('forkX, ql(xname newxname newgname toks),
**** restart the caller once it is forked
                      req('startcListener,ql(xgname 'serializingListener g2dvname), 
                          reqQ1)) 
               else reqQ1 fi)  fi) .

**** chattyocc [udb] | chattyrule t
  op getOccToks : NodeList QidList -> QidList .
  eq getOccToks(ndl,toks) = nil [owise] .
  eq getOccToks(ndl,qid dir toks) = 
      (if checkNodeType(ndl,string(qid),"occ") then qid dir else nil fi)
       getOccToks(ndl,toks) .

  op getRuleToks : NodeList QidList -> QidList .
  eq getRuleToks(ndl,toks) = nil [owise] .
  eq getRuleToks(ndl,qid dir  toks) = 
      (if checkNodeType(ndl,string(qid),"rule") then qid else nil fi) 
      getRuleToks(ndl,toks) .


  op checkNodeType : NodeList String String -> Bool .
  eq checkNodeType(ndl,str,ntype) =
      (if getNode(ndl,"chattylabel",sv(str)) :: Node
       then lookupd(nodeNotes(getNode(ndl,"chattylabel",sv(str))),"type",sv(""))
            == sv(ntype)
       else false 
       fi) .

endm
