{*
* File PN-graphviz.sml
* Author: Manfred Jeusfeld, jeusfeld@uvt.nl
* Date: 2-Jul-2008 (7-Jul-2008)
*----------------------------------------------------------------
* This model file specifies the PetriNet notation and provides and
* export filter for graphviz.
* Steps:
*  1- Load this model into ConceptBase
*  2- Load the example model TrafficLights.sml into ConceptBase
*  3- Ask the query ShowPN[TrafficLights/pn]
*  4- Copy/paste the answer to a file graphviz-input.dot
*  5- Call Graphviz, e.g. by
*       neato -Tpng graphviz-input.dot > graphviz-output.png
* Use the manual pages of dot or neato to learn more about options of Graphviz.
* Graphviz is available from http://graphviz.org/
*
* (c) 2008 by M. Jeusfeld.
* This model file is licensed under the terms of Attribution-Non-Commercial 2.0 Germany
*   http://creativecommons.org/licenses/by-nc/2.0/de/legalcode  (German)
*   http://creativecommons.org/licenses/by-nc/2.0/legalcode     (generic)
* A summary of your rights and obligations concerning this work is available from
*   http://creativecommons.org/licenses/by-nc/2.0/de/deed.en_GB
* Extended rights can be obtained via the author.
*
* Requires ConceptBase 7.1.2 released 8-Jul-2008 or later.
*
*}


{* -------------------------------------------------------------------------- *}
{* Define the Petri Net notation:                                             *}
{*  places, transitions, links between places&transitions, marks              *}
{* -------------------------------------------------------------------------- *}


Place with
  attribute sendsToken: Transition;
  marks: Integer {* defines markings *}
end

Transition with 
  attribute producesToken : Place 
end


{* -------------------------------------------------------------------------- *}
{* Petri Net elements are just all elements that can occur in an              *}
{* Petri Net diagram. We neglect markings here because we do not display them.*}
{* -------------------------------------------------------------------------- *}

PNElement end
Place isA PNElement end
Transition isA PNElement end
Place!sendsToken isA PNElement end
Transition!producesToken isA PNElement end

PNModel in Class with
  attribute
    contains: PNElement
  rule
    r1: $ forall p/Place m/PNModel a/Place!sendsToken
             (m contains p) and Ai(p,sendsToken,a) ==> (m contains a) $;
    r2: $ forall t/Transition m/PNModel a/Transition!producesToken
             (m contains t) and Ai(t,producesToken,a) ==> (m contains a) $
end



{* -------------------------------------------------------------------------- *}
{* We  support the following graphical notation for Petri Nets                *}
{* places                 --> circles                                         *}
{* transitions            --> boxes                                           *}
{* links between the two  --> directed links                                  *}
{* -------------------------------------------------------------------------- *}

GraphVizType end

Boxnode in GraphVizType,Class with
  rule
    r1: $ forall n/Transition (n in Boxnode) $
end
Circlenode in GraphVizType,Class with
  rule
    r1: $ forall n/Place (n in Circlenode) $
end
Link in GraphVizType,Class with
  rule
    r1: $ forall l/Place!sendsToken (l in Link) $;
    r2: $ forall l/Transition!producesToken (l in Link) $
end


{* -------------------------------------------------------------------------- *}
{* ShowPN returns the parameter pn as result. This is apparently not very     *}
{* meaningful but is triggers the evaluation of the answer format script      *}
{* GraphVizPN, which coordinates the production of the answer.                *}
{* -------------------------------------------------------------------------- *}

GenericQueryClass ShowPN isA PNModel with
  required,parameter
     pn: PNModel
  constraint
     c1: $ (pn = this) $
end

{* -------------------------------------------------------------------------- *}
{* ShowElement(pn,type) computes those elements that are contained in a       *}
{* given Petri Net diagram pn and that have the given type (e.g. Boxnode).    *}
{* It is used to format all elements of a Petri Net model to their Graphviz   *}
{* representation.                                                            *}
{* -------------------------------------------------------------------------- *}

GenericQueryClass ShowElement isA PNModel with
  required,parameter
     pn: PNModel;
     type: GraphVizType
  computed_attribute
     elem: PNElement
 constraint
     c1: $ (pn = this) and
           (this contains elem) and
           (elem in type) $
end


{* -------------------------------------------------------------------------- *}
{* GraphVizPN coordinates the production of all Graphviz code for an Petri Net*}
{* diagram. It does so by calling ShowElement for all supported types.        *}
{* -------------------------------------------------------------------------- *}


GraphVizPN in AnswerFormat with
  forQuery q: ShowPN
  head h: 
"# Generated by ConceptBase {cb_version} at {transactiontime}
# Process this file by Graphviz, e.g. 
#    neato -Tpng thisfile.txt > thisfile.png

"
  pattern p:
"digraph {this} \{
{ASKquery(ShowElement[{this}/pn,Boxnode/type],BOXNODE_FORMAT)}
{ASKquery(ShowElement[{this}/pn,Circlenode/type],CIRCLENODE_FORMAT)}
{ASKquery(ShowElement[{this}/pn,Link/type],LINK_FORMAT)}
overlap=false
label=\"PetriNet Model {this}\\\nExtracted from ConceptBase and layed out by Graphviz \"
fontsize=12;
\}
"
end


{* -------------------------------------------------------------------------- *}
{* The following answer formats are linked one-to-one to the supported        *}
{* Graphviz types (Boxnode,...).                                              *}
{* Note that a given Petri Net model referenced by 'this' usually has many    *}
{* elements of a given type. They are scanned by the Foreach-construct.       *}
{* -------------------------------------------------------------------------- *}


{* translation for instances of Boxnode: each is listed behind the *}
{* appropriate Graphviz tag for box nodes.                         *}

BOXNODE_FORMAT in AnswerFormat with
pattern p: "node [shape=box]; {Foreach( ({this.elem}), (n), {n};)}"
end

{* instances of Circlenode are handled analogously. We fix the size *}
{* of the circle, otherwise the size would depend on the label.     *}

CIRCLENODE_FORMAT in AnswerFormat with
pattern p: "node [shape=circle,fixedsize=true,width=0.9]; {Foreach( ({this.elem}), (n), {n};)}"
end

{* Links l have a source From(l) and a destination To(l). *}
LINK_FORMAT in AnswerFormat with
pattern p: "{Foreach( ({this.elem}),(l),{From({l})}->{To({l})};\\n)}"
end