fmod STATUS-AUX is 
  inc GRAPH .
  inc QSTNOTES .
  inc MY-META-ALL .

var n nodeId : Nat .
vars type nid qid : Qid .
vars toks toks' : QidList .
var ?graph : Graph .
vars notes notes' : Notes .
vars id status : String .
vars nds nds' ndl ndl' nodes : NodeList .
var edl : EdgeList .
var occTL : TermList .

******************************************************************************
  op initNodeLAtts : NodeList TermList NodeList -> NodeList .
  op initNotesStatus : Notes TermList -> Notes .

  eq initNodeLAtts(nil,occTL,ndl') = ndl' .
  eq initNodeLAtts(nd(nodeId,notes) ndl,occTL,ndl') =
       initNodeLAtts(ndl,occTL,ndl' nd(nodeId,initNotesStatus(notes,occTL))) .

  eq initNotesStatus(notes,occTL) =
      insert("status",sv("none"),
         (if lookupd(notes,"type",sv("")) == sv("occ") 
             and eltOf(tvalTerm(lookupd(notes,"occ",tm('BOOL,'true.Bool))),
                       occTL)
          then insert("init",sv("true"),notes)
          else notes fi)) .

  op setNodesGoalStatus : NodeList TermList NodeList -> NodeList .
  op setNotesGoalStatus : Notes TermList -> Notes .

  eq setNodesGoalStatus(nil,occTL,ndl') = ndl' .
  eq setNodesGoalStatus(nd(nodeId,notes) ndl,occTL,ndl') =
      setNodesGoalStatus(ndl,occTL,
          ndl' nd(nodeId,setNotesGoalStatus(notes,occTL))) .

  eq setNotesGoalStatus(notes,occTL) =
        (if lookupd(notes,"type",sv("")) == sv("occ") 
            and eltOf(tvalTerm(lookupd(notes,"occ",tm('BOOL,'true.Bool))),
                       occTL)
         then insert("status",sv("goal"),notes)
         else notes fi) .



**** toks are alternating pairs (nid flag)
  sorts Selection SelectionList .
  subsort Selection < SelectionList .
  op (_`,_) : Nat String -> Selection .
  op nil : -> SelectionList .
  op __ : SelectionList SelectionList -> SelectionList [ctor assoc id: nil] .

  var  selects : SelectionList .
  op toks2sel : QidList SelectionList -> SelectionList .
  eq toks2sel( nid qid toks, selects) =
        (if (rat(string(nid),10) :: Nat)
         then toks2sel(toks,selects (rat(string(nid),10), string(qid)))
         else toks2sel(toks, selects)
         fi ) .
  eq toks2sel(toks, selects) = selects [owise] . *** not two left


**** assume (nid status) --- complete status setting
  op setGraphStatus : Graph QidList -> Graph .
  eq setGraphStatus(graph(id,notes,ndl,edl),toks) = 
       graph(id,notes,setNodeLStatus(ndl,toks2sel(toks,nil),nil),edl) .


  op setNodeLStatus : NodeList SelectionList NodeList -> NodeList .
  eq setNodeLStatus(nds' nd(nodeId,notes) nds, (nodeId, status) selects,ndl) =
        setNodeLStatus(nds' nds, selects,
                       ndl nd(nodeId,setNotesStatus(notes,status))) .
  eq setNodeLStatus(nds,(nodeId, status) selects,ndl) = 
         setNodeLStatus(nds, selects,ndl) .  *** no such node 
  eq setNodeLStatus(nds,nil,ndl) = ndl nds .

  op setNotesStatus : Notes String -> Notes .
  eq setNotesStatus(notes,status) =
      (if statusAllowed(notes,status)
       then insert("status", sv(status), notes)
       else notes fi) .

  op statusAllowed : Notes String -> Bool .
  eq statusAllowed(notes, status) =
     (if status == "none" 
      then true
      else (if lookupd(notes,"type",sv("")) == sv("rule")
            then status == "avoid"
            else (lookupd(notes,"type",sv("")) == sv("occ")
****                     and lookupd(notes,"init",sv("false")) == sv("false")
                     and (status == "goal" or status == "avoid"))
            fi )
     fi ) .

**** true ~ set if occ and not init,  false ~ unset if occ and non init and goal
  op setGraphGoals : Graph QidList -> Graph .
  op setNodeLGoals : NodeList SelectionList NodeList -> NodeList .
  op setNotesGoal : Notes String -> Notes .

  eq setGraphGoals(graph(id,notes,ndl,edl),toks) = 
       graph(id,notes,setNodeLGoals(ndl,toks2sel(toks,nil),nil),edl) .
  eq setNodeLGoals(nds nd(nodeId,notes) nds', (nodeId,status) selects, ndl)
     = setNodeLGoals(nds nds',selects,
                     ndl nd(nodeId,setNotesGoal(notes,status))) .
  eq setNodeLGoals(nds,  (nodeId,status) selects, ndl) =
        setNodeLGoals(nds, selects, ndl) [owise] . **** node missing
  eq setNodeLGoals(nds, nil, ndl) = ndl nds .

  eq setNotesGoal(notes,status) = 
       (if lookupd(notes,"type",sv("")) == sv("occ")
           and lookupd(notes,"init",sv("false")) == sv("false")
        then (if status == "true"
              then insert("status", sv("goal"), notes)
              else (if lookupd(notes,"status",sv("none")) == sv("goal")
                    then insert("status", sv("none"), notes) 
                    else notes fi)
              fi)
        else notes
        fi) .


**** true ~ set if  occ and not init, false ~ unset if occ and non init and avoid
  op setGraphAvoids : Graph QidList -> Graph .
  op setNodeLAvoids : NodeList SelectionList NodeList -> NodeList .
  op setNotesAvoid : Notes String -> Notes .

  eq setGraphAvoids(graph(id,notes,ndl,edl),toks) = 
       graph(id,notes,setNodeLAvoids(ndl,toks2sel(toks,nil),nil),edl) .
  eq setNodeLAvoids(nds nd(nodeId,notes) nds', (nodeId,status) selects, ndl)
     = setNodeLAvoids(nds nds',selects,
                     ndl nd(nodeId,setNotesAvoid(notes,status))) .
  eq setNodeLAvoids(nds,  (nodeId,status) selects, ndl) =
        setNodeLAvoids(nds, selects, ndl) [owise] . **** node missing
  eq setNodeLAvoids(nds, nil, ndl) = ndl nds .

  eq setNotesAvoid(notes,status) = 
       (if lookupd(notes,"type",sv("")) == sv("occ")
           and lookupd(notes,"init",sv("false")) == sv("false")
        then (if status == "true"
              then insert("status", sv("avoid"), notes)
              else (if lookupd(notes,"status",sv("none")) == sv("avoid")
                    then insert("status", sv("none"), notes) 
                    else notes fi)
              fi)
        else notes
        fi) .

**** true ~ set if  rule, false ~ unset if rule
  op setGraphHides : Graph QidList -> Graph .
  op setNodeLHides : NodeList SelectionList NodeList -> NodeList .
  op setNotesHide : Notes String -> Notes .

  eq setGraphHides(graph(id,notes,ndl,edl),toks) = 
       graph(id,notes,setNodeLHides(ndl,toks2sel(toks,nil),nil),edl) .
  eq setNodeLHides(nds nd(nodeId,notes) nds', (nodeId,status) selects, ndl)
     = setNodeLHides(nds nds',selects,
                     ndl nd(nodeId,setNotesHide(notes,status))) .
  eq setNodeLHides(nds,  (nodeId,status) selects, ndl) =
        setNodeLHides(nds, selects, ndl) [owise] . **** node missing
  eq setNodeLHides(nds, nil, ndl) = ndl nds .

  eq setNotesHide(notes,status) = 
       (if lookupd(notes,"type",sv("")) == sv("rule")
        then (if status == "true"
              then insert("status", sv("avoid"), notes)
              else insert("status", sv("none"), notes) 
              fi)
        else notes
        fi) .

**** sets all status attributed to "none"
  op resetGraphStatus : Graph -> Graph .
  eq resetGraphStatus(graph(id,notes,ndl,edl)) = 
       graph(id,notes,
              resetNodesStatus(ndl,nil),
              edl) .

  op resetNodesStatus : NodeList NodeList -> NodeList .
  op resetNotesStatus : Notes -> Notes .
  eq resetNodesStatus(nil,nodes) = nodes .
  eq resetNodesStatus(nd(nodeId,notes) nds,nodes) = 
      resetNodesStatus(nds,
                      nodes nd(nodeId,insert("status", sv("none"), notes) )) . 


endfm
