| Both sides previous revisionPrevious revisionNext revision | Previous revision |
| help:scripting [2024/11/13 09:16] – Add mutex protocol transformation commands danil | help:scripting [2026/05/12 10:35] (current) – [Global variables] danil |
|---|
| ==== Global variables ==== | ==== Global variables ==== |
| |
| * ''args'' -- command line parameters passed to Workcraft; these can be iterated over as follows: ''for each (arg in args) {...}'' | * ''args'' -- array of command line parameters passed to Workcraft; these can be iterated over as follows: ''for each (arg in args) {...}'' or accessed as ''args[0]'', ''args[1]'', etc. |
| * ''framework'' -- the Workcraft framework singleton | * ''framework'' -- the Workcraft framework singleton |
| * ''workspaceEntry'' -- the current work | * ''workspaceEntry'' -- the current work |
| |
| * Logic synthesis of Circuits from STGs using Petrify backend | * Logic synthesis of Circuits from STGs using Petrify backend |
| * ''resolveCscConflictPetrify(work)'' -- resolve complete state coding conflicts in the STG 'work' using Petrify | * ''resolveCscConflictPetrify(work)'' -- resolve complete state coding conflicts in the STG ''work'' using Petrify |
| * ''synthComplexGatePetrify(work)'' -- logic synthesis of the STG ''work'' into a complex gate Circuit work using Petrify | * ''synthComplexGatePetrify(work)'' -- logic synthesis of the STG ''work'' into a complex gate Circuit work using Petrify |
| * ''synthGeneralisedCelementPetrify(work)'' -- synthesis of the STG ''work'' into a generalised C-element Circuit using Petrify | * ''synthGeneralisedCelementPetrify(work)'' -- synthesis of the STG ''work'' into a generalised C-element Circuit using Petrify |
| |
| * Logic synthesis of Circuits from STGs using MPSat backend | * Logic synthesis of Circuits from STGs using MPSat backend |
| * ''resolveCscConflictMpsat(work)'' -- resolve complete state coding conflicts in the STG 'work' using MPSat | * ''resolveCscConflictMpsat(work)'' -- resolve complete state coding conflicts in the STG ''work'' using MPSat |
| * ''synthComplexGateMpsat(work)'' -- logic synthesis of the STG ''work'' into a complex gate Circuit work using MPSat | * ''synthComplexGateMpsat(work)'' -- logic synthesis of the STG ''work'' into a complex gate Circuit work using MPSat |
| * ''synthGeneralisedCelementMpsat(work)'' -- synthesis of the STG ''work'' into a generalised C-element Circuit work using MPSat | * ''synthGeneralisedCelementMpsat(work)'' -- synthesis of the STG ''work'' into a generalised C-element Circuit work using MPSat |
| * Commands specific for Circuit models | * Commands specific for Circuit models |
| * ''checkCircuitBinateImplementation(work)'' -- check the Circuit ''work'' for correct implementation of its binate functions <wrap info>since **v3.2.5**</wrap> | * ''checkCircuitBinateImplementation(work)'' -- check the Circuit ''work'' for correct implementation of its binate functions <wrap info>since **v3.2.5**</wrap> |
| * ''checkCircuitCombined(work)'' -- combined check of the Circuit ''work'' for conformation to environment, deadlock freeness, and output persistency | * ''checkCircuitCombined(work)'' -- combined check of the Circuit ''work'' for all essential properties (conformation to environment, output persistency, deadlock freeness) |
| * ''checkCircuitConformation(work)'' -- check the Circuit ''work'' for conformation to environment | * ''checkCircuitConformation(work)'' -- check the Circuit ''work'' for conformation to environment |
| * ''checkCircuitCycles(work)'' -- check if the Circuit ''work'' is free from cyclic paths | * ''checkCircuitCycles(work)'' -- check if the Circuit ''work'' is free from cyclic paths |
| |
| * Commands specific for STG models | * Commands specific for STG models |
| * ''checkStgCombined(work)'' -- combined check of the STG ''work'' for consistency, deadlock freeness, input properness, output persistency, and mutex implementability | * ''checkStgCombined(work)'' -- combined check of the STG ''work'' for all essential properties (consistency, output determinacy, input properness, mutex protocol, output persistency, absence of local self-triggering, deadlock freeness, delay insensitive interface) |
| * ''checkStgConformation(work, data)'' -- check the STG ''work'' for conformation to the STG specified by file name ''data'' <wrap info>since **v3.3.0**</wrap> | * ''checkStgConformation(work, data)'' -- check the STG ''work'' for conformation to the STG specified by file name ''data'' <wrap info>since **v3.3.0**</wrap> |
| * ''checkStgConsistency(work)'' -- check the STG ''work'' for consistency | * ''checkStgConsistency(work)'' -- check the STG ''work'' for consistency |
| * ''checkStgCsc(work)'' -- check the STG ''work'' for CSC | * ''checkStgCsc(work)'' -- check the STG ''work'' for CSC |
| * ''checkStgDeadlockFreeness(work)'' -- check the STG (or Petri net) ''work'' for deadlock freeness | * ''checkStgDeadlockFreeness(work)'' -- check the STG (or Petri net) ''work'' for deadlock freeness |
| * ''checkStgDiInterface(work)'' -- check the STG ''work'' for DI interface | * ''checkStgDiInterface(work)'' -- check the STG ''work'' for delay insensitive interface |
| * ''checkStgHandshakeProtocol(work, data)'' -- check the STG ''work'' for following a handshake protocol as specified by ''data'', e.g. ''{req1 req2} {ack12}'' <wrap info>since **v3.3.0**</wrap> | * ''checkStgHandshakeProtocol(work, data)'' -- check the STG ''work'' for following a handshake protocol as specified by ''data'', e.g. ''{req1 req2} {ack12}'' <wrap info>since **v3.3.0**</wrap> |
| * ''checkStgInputProperness(work)'' -- check the STG ''work'' for input properness | * ''checkStgInputProperness(work)'' -- check the STG ''work'' for input properness |
| | * ''checkStgLocalSelfTriggering(work)'' -- check the STG ''work'' for absence of local self-triggering |
| * ''checkStgMutexImplementability(work)'' -- check the STG ''work'' for implementability of its mutex places | * ''checkStgMutexImplementability(work)'' -- check the STG ''work'' for implementability of its mutex places |
| * ''checkStgNormalcy(work)'' -- check the STG ''work'' for normalcy | * ''checkStgNormalcy(work)'' -- check the STG ''work'' for normalcy |
| * ''checkStgOutputDeterminacy(work)'' -- check the STG ''work'' for output determinacy | * ''checkStgOutputDeterminacy(work)'' -- check the STG ''work'' for output determinacy |
| * ''checkStgOutputPersistency(work)'' -- check the STG ''work'' for output persistency | * ''checkStgOutputPersistency(work)'' -- check the STG ''work'' for output persistency |
| * ''checkStgPlaceRedundancy(work, data)'' -- check the STG (or Petri net) 'work' for redundancy of places in space-separated list ''data'' <wrap info>since **v3.3.0**</wrap> | * ''checkStgPlaceRedundancy(work, data)'' -- check the STG (or Petri net) ''work'' for redundancy of places in space-separated list ''data'' <wrap info>since **v3.3.0**</wrap> |
| * ''checkStgReachAssertion(work, data)'' -- check the STG ''work'' for REACH assertion ''data'' <wrap info>since **v3.3.0**</wrap> | * ''checkStgReachAssertion(work, data)'' -- check the STG ''work'' for REACH assertion ''data'' <wrap info>since **v3.3.0**</wrap> |
| * ''checkStgSignalAssertion(work, data)'' -- check the STG ''work'' for signal assertion ''data'' <wrap info>since **v3.3.0**</wrap> | * ''checkStgSignalAssertion(work, data)'' -- check the STG ''work'' for signal assertion ''data'' <wrap info>since **v3.3.0**</wrap> |
| |
| * Generic commands applicable to all models | * Generic commands applicable to all models |
| | * ''transformModelAnonymise(work)'' -- anonymise the model ''work'' by randomly renaming its nodes |
| * ''transformModelCopyLabel(work)'' -- transform the model ''work'' by copying unique names of the selected (or all) nodes into their labels | * ''transformModelCopyLabel(work)'' -- transform the model ''work'' by copying unique names of the selected (or all) nodes into their labels |
| * ''transformModelStraightenConnection(work)'' -- transform the model ''work'' by straightening selected (or all) arcs | * ''transformModelStraightenConnection(work)'' -- transform the model ''work'' by straightening selected (or all) arcs |
| * ''transformDfsContractComponent(work)'' -- transform the DFS ''work'' by contracting selected components | * ''transformDfsContractComponent(work)'' -- transform the DFS ''work'' by contracting selected components |
| * ''transformDfsMergeComponent(work)'' -- transform the DFS ''work'' by merging selected components | * ''transformDfsMergeComponent(work)'' -- transform the DFS ''work'' by merging selected components |
| | * ''transformDfsSplitComponent(work)'' -- transform the DFS ''work'' by splitting selected components <wrap info>since **v3.5.2**</wrap> |
| * ''transformDfsWagging2Way(work)'' -- transform the DFS ''work'' by applying 2-way wagging to the selected pipeline section | * ''transformDfsWagging2Way(work)'' -- transform the DFS ''work'' by applying 2-way wagging to the selected pipeline section |
| * ''transformDfsWagging3Way(work)'' -- transform the DFS ''work'' by applying 3-way wagging to the selected pipeline section | * ''transformDfsWagging3Way(work)'' -- transform the DFS ''work'' by applying 3-way wagging to the selected pipeline section |
| * ''transformDfsWagging4Way(work)'' -- transform the DFS ''work'' by applying 4-way wagging to the selected pipeline section | * ''transformDfsWagging4Way(work)'' -- transform the DFS ''work'' by applying 4-way wagging to the selected pipeline section |
| | |
| | * Commands specific for FSM and FST models |
| | * ''transformFsmContractState(work)'' -- transform the FSM/FST ''work'' by contracting selected states |
| | * ''transformFsmSplitState(work)'' -- transform the FSM/FST ''work'' by splitting selected states <wrap info>since **v3.5.2**</wrap> |
| | * transformFsmMergeState''(work)'' -- transform the FSM/FST ''work'' by merging selected states |
| |
| * Commands specific for Petri net and (if explicitly stated) for derived models | * Commands specific for Petri net and (if explicitly stated) for derived models |
| * ''transformStgSelectAllSignalTransitions(work)'' -- select all transitions of selected signals in the STG ''work'' | * ''transformStgSelectAllSignalTransitions(work)'' -- select all transitions of selected signals in the STG ''work'' |
| * ''transformStgSignalToDummyTransition(work)'' -- transform the STG ''work'' by converting selected signal transitions to dummies | * ''transformStgSignalToDummyTransition(work)'' -- transform the STG ''work'' by converting selected signal transitions to dummies |
| | * ''transformStgSplitTransition(work)'' -- transform the STG ''work'' by splitting selected transitions <wrap info>since **v3.5.2**</wrap> |
| |
| * Commands specific for WTG models | * Commands specific for WTG models |
