[ ] 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.
tsl playallows to play against an environment strategy (system strategy) as the system (environment) interactively.tslplayshows 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 checkchecks for a set of TSL specification files, whether they are valid or not.tsl symprints 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 sizeprints 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 splitapplies 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.tslin the current path wherexis the index of the respective subspecification.