User manual/FAQ

From MCRL2

User manual

Introduction Installation instructions Toolset overview Tool manual pages FAQ

Contents

Contents 1 Tools 1.1 Odd crashes on linux 1.2 mcrl22lps: Linearising an untimed mCRL2 file yields an LPS with time 1.3 mcrl22lps: Linearising takes excessively long 1.4 LPS tools: "Cannot enumerate Real" error but no Reals are being used 1.5 LPS tools: Performing tool operations on an LPS created by tbf2lps fails with an assertion 1.6 lpspp: Can I pass the output of lpspp to mcrl22lps? 1.7 LTS tools do not work on very large SVC files 1.8 SQuADT: some tools are missing in the interface 1.9 SQuADT: Windows asks to unblock SQuADT in the firewall 1.10 SQuADT: ltsgraph, ltsview and diagraphica crash when started from SQuADT 1.11 SQuADT 2 Installation 2.1 After `svn update' the toolset no longer builds 2.2 Linux: Visualization tools do not work properly 2.3 Linux: Diagraphica crashes with a segmentation fault at startup 3 Language 3.1 Support for quantifiers 3.2 Support for Reals 3.3 Support for sets and bags 4 Known compilation issues

Tools

Odd crashes on linux

On linux it is advised to set the stacksize to unlimited. This can be done by using a command limit stacksize unlimited. If the stack is limited tools will crash without warning when the stack is full.

mcrl22lps: Linearising an untimed mCRL2 file yields an LPS with time

This issue is caused by the use of the conditional operator c -> p. The default semantics of this operator is c -> p <> delta@0, which introduces time by means of the time stamp 0. When a specification does not contain time, it usually is more sensible to use the alternative semantics c -> p <> delta, that is without the introduction of a time stamp. To use this alternative semantics, the command line option -D/--delta may be used (or you can manually append <> delta to all expressions of the form c -> p).

mcrl22lps: Linearising takes excessively long

There are many potential reasons. First of all, the data equations -- that are considered as rewrite rules (from left to right) -- may not be terminating. Solution is to use the -o/--no-rewrite flag. A second reason can be that removing delta summands is too costly. This is avoided by using the -D/--delta option, which also eliminates timed delta summands. It is also possible that sum elimination is too costly, avoid this using the -m/--no-sumelm flag. The generation of large enumerated data types can also be expensive, which is avoided using the option -b/--binary (this encodes finite datatypes using booleans). Finally, it can be that the translation to regular form is very time consuming. Try to use -lstack/--lin-method=stack option instead of the default -1regular/--lin-method=regular. Also, the use of -lregular2/--lin-method=regular2 results in mcrl22lps terminating more often than the default.

LPS tools: "Cannot enumerate Real" error but no Reals are being used

This issue is most likely caused by the fact that linearisation of an untimed mCRL2 file yielded an LPS with time.

LPS tools: Performing tool operations on an LPS created by tbf2lps fails with an assertion

Currently tbf2lps does not check whether invalid identifiers are inserted into an LPS. Therefore, some tools may fail, as they render an LPS invalid because of this. This issue has at least been seen in lpsactionrename.

lpspp: Can I pass the output of lpspp to mcrl22lps?

Until svn revision 6655, mcrl22lps was not able to read linear process specifications that were pretty printed by lpspp, when the proc or init sections of the resulting specification contained free variable declarations denoted by var. This problem could be circumvented by running mcrl22lps with the -f/--no-freevars option, but it was not recommended when running other LPS tools. As of revision 6656, mcrl22lps is able to handle global variables, which replace the notion of free variables.

LTS tools do not work on very large SVC files

When using lps2lts the default mCRL2 (SVC-based) format can only be used when storing state spaces that fit into 4GiB. Files containing state spaces larger than that become unusable by any of the tools.

SQuADT: some tools are missing in the interface

When SQuADT is executed for the first time, it tries to find the required tools. If they cannot be found automatically, a pop-up appears which asks a user to guide SQuADT to the tools, by selecting a required one.

When tools are missing in SQuADT, please remove the .squadt/tool_catalog file in your "home" directory and restart SQuADT.

1. On Linux/Unix: $HOME/.squadt/tool_catalog
2. On Windows XP: C:\Documents and Settings\user\.squadt\tool_catalog
3. On Mac OS X: /Users/user/.squadt/tool_catalog

Prior to the installation of a new version of the toolset, we advise users to remove .squadt directory.

SQuADT: Windows asks to unblock SQuADT in the firewall

SQuADT internally uses socket communication to connect to the specific mCRL2 tools. This causes the Windows firewall to ask to unblock SQuADT. By default SQuADT will only connect to localhost (127.0.0.1), and will never connect to the internet. Failing to unblock SQuADT in the firewall may lead to malfunction.

SQuADT: ltsgraph, ltsview and diagraphica crash when started from SQuADT

It is currently known that ltsgraph, ltsview and diagraphica crash when they are started from SQuADT in Windows Vista and Windows 7. A proper fix for this is currently not available. To work around this issue you can manually start the tools (from the start menu -> mCRL2 -> { ltsgraph, ltsview, diagraphica }), and manually open the file you want to display.

SQuADT

SQuADT is an alpha-tool, that may display inconsistent behavior. This may result in wrong user feedback, e.g. wrongful coloring of files, no feedback when tools are started or exit unexpectedly. Known issues are listed here.

Installation

After `svn update' the toolset no longer builds

Sometimes changes to the build system that are imported when running svn update cause build failures. Some different causes:

• accidental committed mistakes
• targets from different build configurations (e.g. x86 vs. x86-x64, Release vs. Debug) reside in same build tree
• configuration has changed

When the configure has changed, CMake should automatically trigger a new configuration. It is possible to trigger it manually by executing `cmake ." from the build-tree. If the problem persists, it is possible to remove the build target by executing `make clean'. This will preserve the current configuration. As a last resort it is possible to create a new build tree. This will require you to configure the build tree from scratch.

Linux: Visualization tools do not work properly

OpenGL tools do not work properly on X servers that use a Composite window manager (like Compiz or Beryl). Unfortunately this is a widespread issue that affects all OpenGL applications in general, not just the mCRL2 tools. We know of no workaround for this problem other than disabling your Composite window manager.

Linux: Diagraphica crashes with a segmentation fault at startup

With ATI cards diagraphica can terminate with a segmentation fault during initialization. Possible solutions:

• 1. Set the LD_PRELOAD environment variable to libGL.so.1.2 which is usually located in /usr/lib/. Depending on your shell you can start diagraphica with the following command:

     LD_PRELOAD=/usr/lib/libGL.so.1.2 diagraphica 

     or by

     setenv LD_PRELOAD /usr/lib/libGL.so.1.2

     diagraphica 

     Note: Setting LD_PRELOAD may cause instability to other programs
  2. On Novel/SuSE-10.2-IA32: Install the proprietary ATI drivers via YaST.
     • Start "YaST Control Center" → "Software" → "Installation Source" → "Add source".
     • Use the following configuration:
       • Protocol: HTTP
       • Server Name: www2.ati.com
       • Directory and Server: /SuSE/10.2
     • After the source has been added, go to "YaST Control Center" → "Software" → "Software Managment".
     • Depending on the flavour of your kernel install the following packages:
       • ati-fglrxG01-kmp-default-<kernel-version>
       • x11-video-fglrxG01

     where <kernel-version> can be determined using: uname -r.

     • After installing, go to runlevel 3 ("#init 3") and start sax2 using: sax2 -r.
     • Test and save your configuration and restart your X-server.

Language

Support for quantifiers

As it stands, the implementation of quantifiers (exists and forall) in the language is not very advanced. This means that they can be used, but in general, simulating an mCRL2 model, or generating a state space for an mCRL2 model with quantifiers will most likely not succeed.

Support for Reals

The implementation of reals is currently the same as the implementation of integers, which explains the current lack of specific operators on reals.

Support for sets and bags

Sets over sort A are internally represented using functions of sort A -> Bool, and bags are represented by functions of sort A -> Nat. Currently, sets and bags are not normalized, meaning that two equal sets can have different denotations. For instance the empty set {} and the empty set to which an element is added that is subsequently removed again are not syntactically the same objects in memory. This means that sets and bags are suitable for simulation of processes, but as it stands not yet suited for state space generation. For state space generation it is generally better to use lists.

Known compilation issues

LTSview will produce a segmentation fault when loading a file if being compiled with MSVC9. Compiling LTSview with either MinGW or MSVC10 resolves the segmentation fault.

---

txt2pbes