Formalism

Graph Markup Language (GrML)

A model is an instance of a formalism. It is represented in XML format according to the structure of a graph. A model thus contains nodes and arcs, the arcs making it possible to connect the nodes. Attributes are attached to the model as well as to all elements of the model. These attributes define information about the model (name, author, etc.) or the elements (name, valuation, etc.).

The element allows to manage the hierarchical models and composition can be done with elementary references. The formalismUrl, nodeType, and arcType attributes allow to independently determine the structure of the format that is used as well as the different types of elements that make up the model.

Meta Model Diagram

Validate GrML file

You can use the model.rng file to validate any GrML file.

> xmllint --noout --relaxng model.rng <grml file>

Example

<?xml version="1.0" encoding="UTF-8"?>

<model formalismUrl="ptnet++.fml" xmlns="http://cosyverif.org/ns/model">

  <node id="1" nodeType="place">
    <attribute name="name">Place</attribute>
    <attribute name="marking">1</attribute>
  </node>
  <node id="2" nodeType="virtualPlace">
    <attribute name="name">Ref</attribute>
    <ref href="?id=1"/>
  </node>
  <node id="3" nodeType="transition">
    <attribute name="name">Transition</attribute>
  </node>

  <arc id="4" arcType="arc" source="1" target="3"/>
  <arc id="5" arcType="arc" source="3" target="2"/>
</model>

Formalism Markup Language (FML)

A formalism is a structured document (XML) that has to respect a certain syntax. it allows to specify the different types of supported elements (e.g., nodes and arcs). Moreover, it also allows to specify the different types of attributes related to the model and to the different types of elements.

A formalism can be abstract. A model cannot be of an abstract type since an abstract formalism is a part of another formalism. FML allows to include the definition of another formalism (abstract or not).

Hierarchical formalism can specify the types of hierarchies allowed by specifying which types of nodes and arcs can contain references. The type of the referenced element is also specified using the targetUrl attribute.

Meta Model Diagram

Validate FML file

You can use the formalism.rng file to validate any FML file.

> xmllint --noout --relaxng formalism.rng <fml file>

Example

<?xml version="1.0" encoding="UTF-8"?>

<formalism name="Place/Transition Net" xmlns="http://cosyverif.org/ns/formalism">
  <nodeType name="place"/>
  <leafAttribute name="name" refType="place"/>
  <leafAttribute name="initialMarking" defaultValue="0" refType="place"/>

  <nodeType name="transition"/>
  <leafAttribute name="name" refType="transition"/>

  <arcType name="arc"/>
  <leafAttribute name="valuation" refType="arc"/>
</formalism>