title
author
November 2018
Version
ldlmc -- model-checker for LDL
Table of Contents
Synopsis
Description
Options
See Also
Author
Copyright
Synopsis
ldlmc
*
?
Description
ldlmc reads a model M (from
) in LDL and a LDL formula φ (from
), examines if M ⊨ φ (i.e., ⊨ M → φ) holds or not, and then returns either "claim holds" (M ⊨ φ holds) or "claim does not hold"
Options
--model
reads a model from
--reachability
check reachability (i.e., M ∧ φ ≠ empty), instead of entailment.
-v
,
--verbose
become verbose
-h
,
--help
show usage
See Also
ldlsat, ldl2mso
Author
https://ldltools.github.io
ldltools@outlook.com
Copyright
(C) Copyright IBM Corp. 2018.