fmod GRAPH2LOLA is
  inc GRAPH .
  inc SVAL .
  inc NAT-QID .

***(
PLACES p0, p1, p2, p3, p4, p5;

MARKING p0 : 1, p1 : 0, p4 : 1;

TRANSITION t64
CONSUME p80 : 1, p30 : 1, p68 : 1, p84 : 1, p1 : 1;
PRODUCE p80 : 1, p30 : 1, p68 : 1, p84 : 1, p81 : 1;
...
)

  vars att val def ?string : String .
  vars pathStr preStr postStr placesStr initStr transStr : String .
  var nds : NodeList .
  vars n nodeId : Nat .
  var notes : Notes .
  vars nodes nodes' occNodes initNodes ruleNodes : NodeList .
  var edges : EdgeList .
  vars start end : FindResult .
  vars rids qids : QidList .
  var nid : Qid .

*** Assume graph of relevant subnet with init and goal status marked

  op mkLolaNetString     : Graph  -> String .
  op mkLolaNetString     : NodeList  -> String .
  op mkLolaPlacesString  : NodeList String -> String .
  op mkLolaMarkingString : NodeList String -> String .
  op mkLolaTransString   : NodeList String -> String .
  op mkLolaTrans1        : Nat Notes -> String .
  op mkLolaPrePost       : QidList -> String .

  eq mkLolaNetString(graph(?string,notes,nodes,edges)) =
       mkLolaNetString(nodes) .
  ceq mkLolaNetString(nodes) =
      placesStr + initStr + transStr 
   if occNodes := getNodes(nodes,"type",sv("occ"))
   /\ initNodes := getNodes(occNodes,"init", sv("true"))
   /\ ruleNodes := getNodes(nodes,"type",sv("rule"))
   /\ placesStr := mkLolaPlacesString(occNodes,"PLACE ") + ";\n" 
   /\ initStr := mkLolaMarkingString(initNodes, "\nMARKING ") + ";\n" 
   /\ transStr := mkLolaTransString(ruleNodes, "") 
  .

  eq mkLolaPlacesString(nil, ?string) = ?string .
  eq mkLolaPlacesString(nd(nodeId,notes) nds, ?string) = 
         mkLolaPlacesString(nds,
           (if nds == nil 
            then ?string + "p" + string(nodeId,10)
            else ?string + "p" + string(nodeId,10) + ", "
            fi)) .

  eq mkLolaMarkingString(nil, ?string) = ?string .
  eq mkLolaMarkingString(nd(nodeId,notes) nds, ?string) = 
         mkLolaMarkingString(nds,
           (if nds == nil 
            then ?string + "p" + string(nodeId,10) + " : 1"
            else ?string + "p" + string(nodeId,10) + " : 1" + ", "
            fi)) .

  eq mkLolaTransString(nil, ?string) = ?string .
  eq mkLolaTransString(nd(nodeId,notes) nds, ?string) = 
         mkLolaTransString(nds, ?string + mkLolaTrans1(nodeId,notes)) .

  ceq mkLolaTrans1(nodeId,notes) = 
      "TRANSITION " + "t" + string(nodeId,10) + "\n"
       + "CONSUME " + mkLolaPrePost(str2qidl(preStr)) + ";\n"
       + "PRODUCE " + mkLolaPrePost(str2qidl(postStr)) + ";\n"
  if sv(preStr) := lookupd(notes,"pre",sv(""))
  /\ sv(postStr) := lookupd(notes,"post",sv("")) .

  eq mkLolaPrePost(nil) = "" .
  eq mkLolaPrePost(nid qids) = 
      "p" + string(nid) + " : 1" +
     (if qids == nil then "" else ", " + mkLolaPrePost(qids) fi) .


**** FORMULA ( (p72 = 1) AND  (p73 = 1) )

  op mkLolaTaskString : Graph -> String .
  op mkLolaTaskString : NodeList -> String .
  op mkLolaGoalString : NodeList -> String .
  
  eq mkLolaTaskString(graph(?string,notes,nodes,edges)) =
          mkLolaTaskString(nodes) .

  eq mkLolaTaskString(nodes)
     =
   "FORMULA ( " + 
      mkLolaGoalString(getNodes(getNodes(nodes,"type",sv("occ")),
                        "status",sv("goal"))) 
      + " )\n" .

  eq mkLolaGoalString(nil) = "" .
  eq mkLolaGoalString(nd(nodeId,notes) nds) = 
      "( " + "p" + string(nodeId,10) + " = 1 )" 
      + (if nds == nil then "" else " AND " + mkLolaGoalString(nds) fi) .   

****HERE!!!
**** Parsing Lola output
**** "PATH t0 t15 ... "

  op readLolaResult : NodeList QidList -> QidList . **** the transitions fired
  op getLolaTrans : NodeList QidList -> QidList . 
 
  eq readLolaResult(nodes, qids) = 
     (if (size(qids) <= 2)
      then nil
      else getLolaTrans(nodes, getPost(2,qids)) fi) .
 ****  skip the code and initial PATH 

  eq getLolaTrans(nodes,nil) = nil .
  ceq getLolaTrans(nodes,nid qids) = 
        ( rids getLolaTrans(nodes,qids)  )
      if ?string := substr(string(nid),1,length(string(nid)))
      /\ n := rat(?string,10) 
      /\ nodes' := (if n :: Nat then getNode(nodes,n) else nil fi)
      /\ rids := 
            (if nodes' :: Node
             then qid(svalString(lookupd(nodeNotes(nodes'),
                                         "chattylabel",sv("")))) 
                  else nil fi)
      .


*** Assume graph of relevant subnet with init and goal status marked


***(
  op mkLola2NetString     : Graph  -> String .
  eq mkLola2NetString(graph(?string,notes,nodes,edges)) =
       mkLola2NetString(nodes) .
)

  op mkLola2NetString     : NodeList  -> String .
  op mkLola2PlacesString  : NodeList String -> String .
  op mkLola2MarkingString : NodeList String -> String .
  op mkLola2TransString   : NodeList String -> String .
  op mkLola2Trans1        : Nat Notes -> String .
  op mkLola2PrePost       : QidList -> String .

  ceq mkLola2NetString(nodes) =
      placesStr + initStr + transStr 
   if occNodes := getNodes(nodes,"type",sv("occ"))
   /\ initNodes := getNodes(occNodes,"init", sv("true"))
   /\ ruleNodes := getNodes(nodes,"type",sv("rule"))
   /\ placesStr := mkLola2PlacesString(occNodes,"PLACE SAFE 1: ") + ";\n" 
   /\ initStr := mkLolaMarkingString(initNodes, "\nMARKING ") + ";\n" 
   /\ transStr := mkLolaTransString(ruleNodes, "") 
  .

  eq mkLola2PlacesString(nil, ?string) = ?string .
  eq mkLola2PlacesString(nd(nodeId,notes) nds, ?string) = 
         mkLola2PlacesString(nds,
           (if nds == nil 
            then ?string + "p" + string(nodeId,10)
            else ?string + "p" + string(nodeId,10) + ", "
            fi)) .

**** EF ( (p72 = 1) AND  (p73 = 1) )
***(
  op mkLola2TaskString : Graph -> String .
  eq mkLola2TaskString(graph(?string,notes,nodes,edges)) =
          mkLola2TaskString(nodes) .
)
  op mkLola2TaskString : NodeList -> String .
  op mkLola2GoalString : NodeList -> String .
  

  eq mkLola2TaskString(nodes)
     =
   "EF ( " + 
      mkLolaGoalString(getNodes(getNodes(nodes,"type",sv("occ")),
                        "status",sv("goal"))) 
      + " )\n" .

endfm



