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
But running "lps2pbes .lps .mcf --check-only" does actually work. It nicely prints whether the formula is well-formed. The shorthand flag -e also works.
The documentation should be updated.
The text was updated successfully, but these errors were encountered:
This is a hidden option that can be found by running lps2pbes --help-all. This is also the reason it is not included in the documentation. If there are good reasons to expose it, we could decide to unhide this option.
I implemented this some time ago (see 3a06842) because I needed it for mCRL2IDE, but I can't remember why we decided for it to be hidden though. The tool mcrl22lps has a similar option for checking an mCRL2 spec which is not hidden, so I can imagine we can just make this one non-hidden as well.
I can imagine wanting to hide experimental features or features that have very limited use cases. But I think being able to check a formula is a pretty normal functionality.
My use case: I use a number of Python scripts to orchestrate the mCRL2 toolset. I also use a script to check whether all the mu-calculus formulas in a predefined directory are valid.
The documentation does not state that lps2pbes can be used to only check a formula: https://mcrl2.org/web/user_manual/tools/release/lps2pbes.html
But running "lps2pbes .lps .mcf --check-only" does actually work. It nicely prints whether the formula is well-formed. The shorthand flag -e also works.
The documentation should be updated.
The text was updated successfully, but these errors were encountered: