dsl4sc
dsl4sc is a domain-specific language, based on LDLf, for defining and verifying state transition models for event processing.
Command-line tools
rulessat
usage: rulessat <model>.dsl
rulessat solves the satisfiability of the input DSL4SC model included in <model>.dsl and returns either valid, satisfiable, or unsatisfiable.
See this manual for the detail.
rulesmc
usage: rulesmc -m <model>.dsl <property>.dsl
Given a model and a property in DSL4SC,
rulesmc checks whether model ⊨ property (entailment) holds or not.
In case you need to examine if property can hold,
that is,
model ∧ property is satisfiable (reachability),
invoke rulesmc with the --reachability option.
See this manual for the detail.
rules2scxml
usage: rules2scxml <model>.dsl
rules2scxml translates the input DSL4SC model into an equivalent UML statechart representation in the SCXML format.
As a remark, rules2scxml performs translation through several intermediate stages, at each of which translation can be terminated. Refer to this for the detail.
safeguard
usage: safeguard --spec <model>.dsl <code>.js
safeguard generate pre/post conditions from <model>.dsl for event-handlers defined in <code>.js, and insert them into the code.
Models in DSL4SC
Each model definition should conform to the DSL4SC grammar.
Note that LDLf-related parts, namely ldl_formula and ldl_path, of the grammar is defined separetely elsewhere.
As a remark, there exists another simplified version of the grammar, called the DSL4SC core grammar, which is used internally by the tools listed above.
