Syntax of the Model File

	  <nycs>
	    <component id="name of the LHG">
	      list of variables
	      list of locations
	      list of transitions
	    </component>
	  </nycs>
	

• Each variable is declared as follows:

      <param name="variable_name" />
    

  Every variable must be declared before its use.
• Each location is declared as follows:

      <location id="loc_id" name="loc_name">
         <flow> convex polyhedron on primed variables </flow>
         <invariant> polyhedron on unprimed variables </invariant>
      </location>
    

  Attributes id and name are used to identify the location. If an invariant is not specified, its value is set to "true". Every location has to be declared before its transitions.
• Each transition is declared as follows:

      <transition source="source_location_id" target="target_location_id" >
         <contr>true or false</contr>
         <guard>polyhedron on unprimed variables </guard>
         <assignment>convex polyhedron on primed and unprimed variables</assignment>
      </transition >
    

  Attributes source and target contain the IDs of the source and target location, respectively. Moreover:
  • The contr attribute specifies if the transition is controllable (attribute value "true") or uncontrollable (attribute value "false"). Default is "false" (uncontrollable).
  • The guard section describes the variable valuations for which the transition is enabled.
  • The assignment section describes the new value of the variables after the transition. If a primed variable is not mentioned in the assignment (or the assignment section is missing entirely), its value stays the same during the transition. I.e., if variable x' is not mentioned, the constraint x' == x is automatically added.

Model file example

Notice: XML requires characters <, >, and & to be encoded as "&lt;", "&gt;", and "&amp;", respectively. Scripts txt2xml.sh and xml2txt.sh in the bin folder help convert between simple text and XML.

Example of a model file: