Missing documentation --check-only flag lps2pbes

[markuzzz]

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.

[tneele]

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.

[Valo13]

I implemented this some time ago (see 3a06842c44edf10da2ebbb1f699964b3e4f71952) 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.

[markuzzz]

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.