tina-3.2.0（linux最新版本）for Petri

formats(n) formats(n) NAME formats - file formats of the Tina Toolbox Part of Tina Toolbox for analysis of Petri nets and Time Petri nets. DESCRIPTION This page describe the formats of files used by the Tina tools. Time Petri nets formats, input of tina/sift/struct/plan/play/ndrio/nd: net.txt .net Time Petri nets textual format ndr.txt .ndr Time Petri nets graphic format tpn.txt .tpn Time Petri nets script format pnml.txt .pnml Time Petri nets pnml format Time Transition System format, input of tina/sift/struct/plan/play (not supported by ndrio nor nd): tts.txt .tts Time Transition System format Transition system formats, output of tina: aut.txt .aut Transition systems textual format (CADP format) ktz.txt .ktz Kripke transition systems binary format (tina) bcg.txt .bcg Transition systems binary format (tina for CADP) mec.txt .mec Kripke transition systems textual format (tina for MEC4) Other formats: adr.txt .adr Transition systems graphic format (nd) ltl.txt .ltl SE-LTL model checker commands (selt) mmc.txt .ltl Mu-calculus model checker commands (muse) scn.txt .scn Format of firing sequences and firing schedules, (selt, plan, play, nd stepper history files) The .net format This is the textual description format of Time Petri nets. A net is described by a series of declarations of places and/or transitions, and an optional naming declaration for the net. The net described is the superposition of these declarations. The grammar of .net declarations is the following, in which nonterminals are bracketed by < .. >, terminals are in upper case or quoted. Spaces, carriage return and tabs act as separators. Optionally, labels may be assigned to places and transitions. This should be preferably done within "tr" and "pl" declarations rather than using separate "lb" declarations. The later form ("lb") is kept for backward compatibility and might disappear in future releases. Grammar: .net ::= (<trdesc>|<pldesc>|<lbdesc>|<prdesc>|<netdesc>)* netdesc ::= 'net' <net> trdesc ::= 'tr' <transition> {":" <label>} {<interval>} {<tinput> -> <toutput>} pldesc ::= 'pl' <place> {":" <label>} {(<marking>)} {<pinput> -> <poutput>} lbdesc ::= 'lb' [<place>|<transition>] <label> prdesc ::= 'pr' (<transition>)+ ("<"|">") (<transition>)+ interval ::= ('['|']')INT','INT('['|']') | ('['|']')INT','w[' tinput ::= <place>{<arc>} toutput ::= <place>{<normal_arc>} pinput ::= <transition>{<normal_arc>} poutput ::= <transition>{arc} arc ::= <normal_arc> | <test_arc> | <inhibitor_arc> | <stopwatch_arc> | <stopwatch-inhibitor_arc> normal_arc ::= '*'<weight> test_arc ::= '?'<weight> inhibitor_arc ::= '?-'<weight> stopwatch_arc ::= '!'<weight> stopwatch-inhibitor_arc ::= '!-'<weight> weight, marking ::= INT{'K'|'M'} net, place, transition, label ::= ANAME | '{'QNAME'}' INT ::= unsigned integer ANAME ::= alphanumeric name, see Notes below QNAME ::= arbitrary name, see Notes below Notes: Two forms are admitted for net, place and transition names: - ANAME : any non empty string of letters, digits, primes ' and underscores _ - '{'QNAME'}' : any chain between braces, and in which characters {, }, and \ are prefixed by \ Empty lines and lines beginning with '#' are considered comments. In any closed temporal interval [eft,lft], one must have eft <= lft. The letter 'K' (resp. 'M') following a weight or marking multiplies it by 10^3 (resp. 10^6). Weight is optional for normal arcs, but mandatory for test and inhibitor arcs By default: - transitions have temporal interval [0,w[ - normal arcs have weight 1 - places have marking 0 - places and transitin have the empty label "{}" When several labels are assigned to some node, only the last assigned is kept. The .ndr format Format ndr is the format of graphic files produced by the nd editor. A net is described by a series of declarations of places, transitions and edges, followed by a net name declaration. The net described is the superposition of these declarations. Grammar : .ndr ::= (<trdesc>|<pldesc>)* (<edgedesc>|<prdesc>)* <netdesc> trdesc ::= 't' <xpos> <ypos> <transition> <eft> <lft> <anchor> | 't' <xpos> <ypos> <transition> <anchor> <eft> <lft> <anchor> <label> <anchor> pldesc ::= 'p' <xpos> <ypos> <place> <marking> <anchor> {<label> <anchor>} edgedesc ::= 'e' <place> <transition> {<arckind>}<weight> <anchor> | 'e' <place> <ang> <rad> <transition> <ang> <rad> {<arckind>}<weight> <anchor> | 'e' <transition> <place> <weight> <anchor> | 'e' <transition> <ang> <rad> <place> <ang> <rad> <weight> <anchor> prdesc ::= 'e' <transition> <transition> 1 <anchor> | 'e' <transition> <ang> <rad> <transition> <ang> <rad> 1 <anchor> netdesc ::= 'h' <net> {<nodesize> {<bgcolor>}} eft ::= {-}INT lft ::= {-}INT | 'w' weight, marking ::= INT{'K'|'M'} arckind ::= '?' // test (read) arc | '?-' // inhibitor | '!' // stopwatch | '?-' // stopwatch-inhibitor xpos, ypos, rad ::= FLOAT ang ::= UFLOAT net, place, transition, label ::= ANAME | '{'QNAME'}' anchor ::= 'n' | 'nw' | 'w' | 'sw' | 's' | 'se' | 'e' | 'ne' | 'c' FLOAT ::= unsigned float (without exponent) UFLOAT ::= unsigned float between 0 and 1 (without exponent) INT ::= unsigned integer ANAME ::= see notes below QNAME ::= see notes below <nodesize> ::= 'small' | 'normal' | 'large' <bgcolor> ::= any tcl-tk color Notes: Node declarations must precede edge declarations. The last declaration must be the netname declaration (h). Empty lines and lines beginning with '#'are considered comments. A '-' starting an eft or lft denotes an open interval end. In any transition declaration, one must have `lft >= `eft or lft = 'w', where `e denotes e if e>=0, or (-e)-1 otherwise If eft = lft, then they may not be both negative (intervals may not be empty). The letter 'K' (resp. 'M') following a weight or marking multiplies it by 10^3 (resp. 10^6). Two forms are admitted for net, place and transition names: - ANAME : any non empty string of letters, digits, primes ' and underscores _ - '{'QNAME'}' : any chain between braces, and in which characters {, }, and \ are prefixed by \ The .tpn format Format .tpn is a preliminary script language for building nets from net components specified in .net or .ndr format. Syntax of tpn files: A .tpn file is constituted of zero or more lines .tpn ::= <t