******************************************************************************
*** PLA based on IMaude
******************************************************************************
mod PLA-EXPORT is
  inc RFE .
  inc PLA-AUX .
  inc STATUS-AUX .

  inc PNTL2GRAPH .
****  inc GRAPH2G2D .
  inc NEW-GRAPH2G2D .
  inc PRINT-PN .
  inc GRAPH-SBML .


******************************************************************************
*** 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 : Bool .
var n nodeId : Nat .
vars maudename mname g2dname g2dvname kbname modname modname' : Qid .
vars type tkbFname occsFname graphFname nid flag qid : Qid .
vars fname gname pname newgname newpname pathpname dname format : Qid .
vars outQ toks toks' rids srctoks : QidList .
var ?graph : Graph .
vars pntlT pntlT' pnetT occsT ioccsT ioccsT' uoccsT roccsT nT occT : Term .
vars goccsT aoccsT ridsT ugoccsT : Term .
var tl occsTL : TermList .
vars dnotes gnotes pnotes notes : Notes .
vars res0?? res1?? res?? res2?? res3?? : [ResultPair?] .
vars id ?string status str gstr astr rstr title subtitle : String .
vars ctr  ctr1 ctr2 netStr taskStr : String .
vars ndl ndl' nds nodes pndl : NodeList .
var edl : EdgeList .
 
******************************************************************************
*** Graph as lsp
**** writes graph to file (in g2d format)
******************************************************************************

  eq isReq('graph2file) = true .
  eq enabled(wait4s,req('graph2file,ql(gname g2dvname fname toks),reqQ)) = true .

**** assumes dgraph has been made and stored as petri-graph under gname
  rl[graph2file]:
   [nil,
    st(processing(req('graph2file,ql(gname g2dvname fname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewriteX, 
             ql(g2dvname fname 'C graph2fileToks(es,gname,g2dvname)), reqQ')), 
       es,
       log),
       outQ ] .

  op graph2fileToks : ESet Qid Qid -> QidList .
  ceq graph2fileToks(es,gname,g2dvname) = str2toks(?string) 
    if gv(?graph) := getVal(es,'gval,gname,gv(mtGraph)) 
    /\ gnotes := getNotes(es,'gval,gname)
    /\ sv(title) := lookupd(gnotes,"title", sv(string(gname)))
    /\ sv(subtitle) := lookupd(gnotes,"subtitle", sv(""))
    /\ ql(kbname) := lookupd(gnotes,"kbname", ql(gname))
****    /\  ?string :=  mkSavedGraphExp(kbname,?graph,title,subtitle,loadprefix)
     /\  ?string :=  mkSavedNewGraphExp(gname,?graph,gnotes)   
   . 

******************************************************************************
 
******************************************************************************
*** Graph as lsp NEW VERSION
**** writes graph to file (in g2d format)
******************************************************************************

  eq isReq('graph2filex) = true .
  eq enabled(wait4s,req('graph2filex,ql(gname g2dvname fname toks),reqQ)) = true .

**** assumes dgraph has been made and stored as petri-graph under gname
  rl[graph2filex]:
   [nil,
    st(processing(req('graph2filex,ql(gname g2dvname fname toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil,  
    st(ready, wait4s,
       (reqQ 
        req('filewriteX, 
             ql(g2dvname fname 'C graph2filexToks(es,gname,g2dvname)), reqQ')), 
       es,
       log),
       outQ ] .

  op graph2filexToks : ESet Qid Qid -> QidList .
  ceq graph2filexToks(es,gname,g2dvname) = str2toks(?string) 
    if gv(?graph) := getVal(es,'gval,gname,gv(mtGraph)) 
    /\ gnotes := getNotes(es,'gval,gname)
    /\  ?string :=  mkSavedNewGraphExp(gname,?graph,gnotes)  . 

******************************************************************************
  eq isReq('exportGraph) = true .
  eq enabled(wait4s,req('exportGraph,ql(gname g2dvname fname format toks),reqQ)) 
          = true .

  crl[exportgraph]:
   [nil,
    st(processing(req('exportGraph, ql(gname g2dvname fname format toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   (if ?graph == mtGraph
    then [ nil, 
           st(ready, 
              wait4s,
              (reqQ req('msgForUser,
                        ql('exportGraph 'no 'graph gname fname format),reqQ')),
              es,log), 
           outQ ]
     else
      [ nil, 
        st(ready, 
           wait4s,
           (reqQ
            req('filewriteX,
                 ql(g2dvname qid(string(fname) + "." + string(format))
                   'C 
                    str2toks(?string)),
                  reqQ')),
              es,log), 
           outQ ]
     fi)
   if ?graph := gvalGraph(getVal(es,'gval,gname,gv(mtGraph)))
   /\ gnotes := getNotes(es,'gval,gname)
   /\  ql(srctoks) := lookupd(getNotes(es,'gval,gname),"source",ql(nil))
   /\  tm(modname,pnetT)  := getVal(es,'tval, srctoks, tm('BOOL,'true.Bool))
   /\  ?string :=
         (if format == 'sbml
          then mkSBMLNetStr(?graph)
          else (if format == 'pn
                then exportPNet2pn([modname],pnetT)
                else (if format == 'lsp
                      then mkSavedNewGraphExp(gname,?graph,gnotes)  
                      else ""
                      fi) fi)  fi) .

  eq isReq('checkFileWrite) = true .
  eq enabled(wait4s,req('checkFileWrite,ql(qid toks),reqQ)) = true .

crl[checkFileWrite]:
   [nil,
    st(processing(req('checkFileWrite, ql(qid toks),reqQ')), 
       wait4s,reqQ,es,log), 
    outQ]
     =>
   [nil, st(ready,  wait4s, (reqQ reqQ0), es, log), outQ ]
   if reqQ0 :=  
         (if getNth(0,toks,'FAILED) == 'writeOK
          then req('logreq, ql(qid toks),reqQ')
          else req('logreq, ql(qid toks),nil) fi) .


endm
