| Both sides previous revisionPrevious revisionNext revision | Previous revision |
| help:scripting [2024/12/18 15:24] – Add split 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> |
