You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
tsl play allows to play against an environment strategy (system strategy) as the system (environment) interactively. tslplay shows why some options are not available to the user according to the respective specification helping to understand why some specification are unrealizable. The strategies are in the form of a CFM.
tsl check checks for a set of TSL specification files, whether they are valid or not.
tsl sym prints the symbol table that is derived from a TSL specification. The table identifies all inputs, outputs, function, and predicate symbols, as well as their derived type signatures. Therefore, the tool provides a first overview of specified modules. It is, however, also useful to identify typos in the literals used, since they are automatically introduced by their usage and, thus, do not lead to an error if spelled incorrectly.
tsl size prints the size of the specification, i.e., the number of AST nodes of the underlying TSL formula. It can be used for comparing a set of TSL benchmarks.
tsl split applies a sound specification decomposition technique to the give specification. It assumes unrealizability of the negated assumptions (suchthat the spec is not realizable by assumption violation). It saves the resulting specs as <filename>_x.tsl in the current path where x is the index of the respective subspecification.
The text was updated successfully, but these errors were encountered:
tsl play
allows to play against an environment strategy (system strategy) as the system (environment) interactively.tslplay
shows why some options are not available to the user according to the respective specification helping to understand why some specification are unrealizable. The strategies are in the form of a CFM.tsl check
checks for a set of TSL specification files, whether they are valid or not.tsl sym
prints the symbol table that is derived from a TSL specification. The table identifies all inputs, outputs, function, and predicate symbols, as well as their derived type signatures. Therefore, the tool provides a first overview of specified modules. It is, however, also useful to identify typos in the literals used, since they are automatically introduced by their usage and, thus, do not lead to an error if spelled incorrectly.tsl size
prints the size of the specification, i.e., the number of AST nodes of the underlying TSL formula. It can be used for comparing a set of TSL benchmarks.tsl split
applies a sound specification decomposition technique to the give specification. It assumes unrealizability of the negated assumptions (suchthat the spec is not realizable by assumption violation). It saves the resulting specs as<filename>_x.tsl
in the current path wherex
is the index of the respective subspecification.The text was updated successfully, but these errors were encountered: