# new Tcl command makeInaObject [-name xyz] # all methods of an InaObject . help - "No help implemented yet" . version - "2.2" . debug - many stranges lines of output . readNet xyz.pnt - "filename required" - "net already read" - "can't read file: xyz.pnt" . writeNet xyz.pnt - "filename required" - "xyz has no net" - "can't write file: xyz.pnt" . structProps [-placeNames] [-transitionNames] [-printConflicts] - "xyz has no net to analyse" - "there are isolated nodes" . options - list of options and their current setting . options optionname - current setting of optionsname or: - "invalid option: optionname" . options {optionname optionvalue}+ - "Options reset not fully implemented" - "invalid value: optionvalue" . semipositivePlaceInvariants [-dontDeleteSameSupport] [-subInvariants / -surInvariants] [-deleteCovered] [-deleteCoveredSubSur] [-deleteCoveringStrictInvariants] [-useSymmetries] [-showMatrix] [-wantCallback] [-zerosNotPrinted / -nonZeroEntrysOnly / -withNames] [-wantCounterCallback] - "xyz has no net to analyse" - "No proper INVARI.hlp file" - in success number of Invariants is returned as Cardinal . semipositiveTransitionInvariants [-dontDeleteSameSupport] [-subInvariants / -surInvariants] [-deleteCovered] [-deleteCoveredSubSur] [-deleteCoveringStrictInvariants] [-useSymmetries] [-showMatrix] [-wantCallback] [-zerosNotPrinted / -nonZeroEntrysOnly / -withNames] [-wantCounterCallback] - "xyz has no net to analyse" - "No proper INVARI.hlp file" - in success number of Invariants is returned as Cardinal . placeInvariants [-showMatrix] [-wantCallback] [-zerosNotPrinted / -nonZeroEntrysOnly / -withNames] [-wantCounterCallback] - "xyz has no net to analyse" - "only one of formate options possible" - no returnvalue . transitionInvariants [-showMatrix] [-wantCallback] [-zerosNotPrinted / -nonZeroEntrysOnly / -withNames] [-wantCounterCallback] - "xyz has no net to analyse" - "only one of formate options possible" - no returnvalue . getNodeList transition / place - "xyz has no net to analyse" - "node type required" - "type must be one of place or transition" - return a list of all transitions/places . delete . deleteNet . structBound - "xyz has no net to analyse" . deadlockTrapProperty [-placeNames] [-transitionNames] [-wantNodeSetCallback] [-wantLivenessCallback] [-wantCounterCallback] - "xyz has no net to analyse" - "Struct Props must be calculated first" . allComponents [-placeNames] [-transitionNames] [-wantNodeSetCallback] [-wantLivenessCallback] [-wantCounterCallback] - "xyz has no net to analyse" - "Struct Props must be calculated first" . stateMachineCoverability [-placeNames] [-transitionNames] [-wantNodeSetCallback] [-wantLivenessCallback] [-wantCounterCallback] - "xyz has no net to analyse" - "Struct Props must be calculated first" . stateGraph [-depthRestriction number] [-stubbornReduced] [-symmetricReduced] [-precomputedSymmetries] [-computeLiveness] [-computeSCCs] [-computeDynConflicts] [-wantCounterCallback] [-computeOnly] - "xyz has no net to analyse" - "Reachability Graph for xyz already exists" - "insufficient memory for state graph" - returns the number of states calculated . cleanUp - "No clean up necessary for xyz" . tarjanGraph --> this method is mapped to stateGraph and is only supported for backward compatibilty. . CTL [-nottotal] [-noproof] xyzformel_varname - "Formula required" - "xyz has no net to analyse" - " xyz has no stategraph" - "Formula to be checked: xyzformel" - "Checked" - " Formula holds true!" - " Syntax Error x!" - " Place not present !" - " Syntax Error !!" . coverGraph [-depthRestriction] [-symmetricReduced] [-wantCapacityVector] [-wantStateCallback] [-dontPrintStates / -printDeadStates ] [-writePlaceNames] [-writeTransitionNames] [-wantCounterCallback] - "xyz has no net to analyse" - "Coverability Graph for xyz already exists" - "insuffucient memory for cover graph" - returns the number of states calculated . computeSymmetries [-symmetricMarking] [-wantCounterCallback] - "xyz has no net to analyse" - "symmetries for xyz already computed" - "symmetries for xyz can't be computed" - returns a letter corresponding to the result and the number of symmetries found . deleteSymmetries . reachTest [-wantCounterCallback] xyzmarking_varname - "xyz has no net to analyse" - "No marking-list for xyz" - "SubmarkingReachable" or "Reachable" - "SubmarkingNotReachable" or "NotReachable" - "SubmarkingUnknown" or "Unknown" - "Abort" - "no memory" . pollCounter - returns the Last "Zaehler" . stopCalculation --> stops calculation "q to end" . coverTest [-wantCounterCallback] xyzmarking_varname - "xyz has no net to analyse" - "No Graph" - "Nomem" - "No marking-list for xyz" - "Reachable" - "Coverable" - "NotCoverable" - "Unknown" . hasNet - "1" which means it has a net - "0" no net . getName place / transition xyznumber - "xyz has no net to analyse" - "Nodetyp and/or nodenummer are missing" - "Nodetyp must be 'place' or 'transition'" - "Nodenumber must be a Cardinal" - "No name available!" - returns name of xyznumber interpreted as a place / transition . stateEquation [-wantCounterCallback] xyzmarking_varname - "xyz has no net to analyse" - "No marking-list for xyz" - "SubmarkingReachable" or "Reachable" - "SubmarkingNotReachable" or "NotReachable" - "SubmarkingUnknown" or "Unknown" - "Abort" - "no memory" # all Callbacks # (Tcl scipts, called from within the methods) . SetPropCallback property value - property is a number corresponding to a property of the net 1 - ordinary ORD 2 - homogenous HOM 3 - nonblocking multiplicity NBM 4 - pure PUR 5 - conservative CSV 6 - statically conflict-free SCF 7 - connected CON 8 - strongly connected SC 9 - trans. without preplace Ft0 10 - trans. without postplace tF0 11 - place without pretrans. Fp0 12 - place without posttrans. pF0 13 - marked graph MG 14 - state machine SM 15 - free choice FC 16 - extended free choice EFC 17 - extended simple ES 18 - all nonempty traps marked 19 - covered by one minimal T-invariant 20 - Petrinet 21 - subconservative 22 - no deadlock 23 - insufficiently marked deadlock 24 - net contains a token 25 - net contains exactly one token 26 - all SCSM's are marked 27 - covered by SCSM's containing exactly one token each 28 - any minimal deadlock is SCSM 29 - safe 30 - deadlock-trap-property DTP 31 - covered by state machines SMC 32 - covered by scsm's SMD 33 - sm-allocatable SMA 34 - covered by place inv. CPI 35 - covered by trans-inv. CTI 36 - bounded B 37 - structurally bounded SB 38 - resetable, reversible REV 39 - dead state reachable DSt 40 - bad state reachable BSt 41 - dead transition exists DTr 42 - dynamically conflictfree DCF 43 - live L 44 - live if dead trs. ignored LV 45 - live and safe L&S 46 - weakly live WL (only for cpn ) 47 - collectively live CL (only for cpn ) 48 - rank less than NrOfPrevectors - value is either "Y" meaning yes or "N" for no . InvariantCallback type vector - type is a string, describing the invariant semipositivePlaceinvariant semipositiveTransitioninvariant Placeinvariant Transitioninvariant - vector is a string, containing the invariant as a space seperated list . StateCallback type number state - this callback can't be used . NodeSetCallback type number nodeset [attribute] - type is a string, describing the nodeset Deadlock MinimalDeadlock Trap Component MinimalComponent BoundedPlaces - number is a running number for each type, numbers of deadlocks correspond to their traps - nodeset is a string, containing the nodeset as a space seperated list - attribute is a string, describing properties of the nodeset Clean NotSuffMarked StrongConnectedStateMachine StateMachine StrongConnected . CounterCallback - can be used to monitor lengthy computations, has no arguments