

ldlsat

ldlsat is a SAT solver for Linear Dynamic Logic (LDL_f).

Command-line tools

ldlsat

usage: ldlsat <formula>.ldl

ldlsat solves the satisfiability of the input LDL_f formula included in <formula>.ldl and returns either valid, satisfiable, or unsatisfiable.

See this manual for the detail.

ldlmc

usage: ldlmc -m <model>.ldl <property>.ldl

Given a model and a property formula in LDL_f, ldlmc checks whether model ⊨ property (entailment) holds or not.

See this manual for the detail.

ldl2mso

usage: ldl2mso <formula>.ldl

ldl2mso translates the input LDL_f formula into an equivalent MSO representation, which can be passed to mona.

ldlsimp

usage: ldlsimp <formula>.ldl --tac <tac1>,<tac2>,..

This command applies to <formula>.ldl tactics specified by <tac1>,<tac2>,...

LDL_f

LDL_f formulas should conform to the following grammar.

LDL_f grammar (alt: html pdf)

In the ASCII-only form, the grammar is defined as follows.

LDL_f grammar (alt: html pdf)