User manual/FAQ

From MCRL2

User manual

Introduction Installation instructions Toolset overview Tool manual pages FAQ

Contents

Contents 1 Tools 1.1 mcrl22lps: Linearising an untimed mCRL2 file yields an LPS with time 1.2 mcrl22lps: Linearising takes excessively long 1.3 LPS tools: "Cannot enumerate Real" error but no Reals are being used 1.4 LPS tools: Performing tool operations on an LPS created by tbf2lps fails with an assertion 1.5 lpspp: Can I pass the output of lpspp to mcrl22lps? 1.6 LTS tools do not work on very large SVC files 1.7 SQuADT: some tools are missing in the interface 1.8 SQuADT: Windows asks to unblock SQuADT in the firewall 1.9 SQuADT: ltsgraph, ltsview and diagraphica crash when started from SQuADT 1.10 SQuADT 2 Installation 2.1 After `svn update' the toolset no longer builds 2.2 The toolset doesn't build with Boost build 2.3 Linux: Visualization tools do not work properly 2.4 Linux: mCRL2 libraries cannot be found 2.5 Linux: Diagraphica crashes with a segmentation fault at startup 2.6 Windows (MinGW): installation uses wrong directory 2.7 Windows (MinGW): compiling or linking against wxWidgets fails 2.8 Toolset compilation takes a long time 3 Language 3.1 Support for quantifiers 3.2 Support for Reals 3.3 Support for sets and bags 4 Known compile issues

Tools

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:

• there have been changes to the configure script and its output
• changes in the bundled version of the build system
• changes in any of the Jamfile.v2 files

When the configure script is changed it is often necessary to rerun configure and rebuild from a clean source tree. In the other cases it is enough to rebuild from a clean source tree. To clean the source tree remove the build/bin directory (or equivalently run `make clean').

The toolset doesn't build with Boost build

Some people have reported malfunction in the build system that proved to be misconfiguration of Boost Build. The cause is conflicting system wide installation in the form of /etc/site-config.jam.

A problem here is that different Linux distributions configure Boost Build in very different ways. Boost Build v2 itself comes packaged with an empty site-config.jam. But distributions put compiler configurations in this file.

In some cases the existence of the configuration file /etc/site-config.jam means that config.jam should not include the toolset.using rule invocation; but in others it must be there. When Boost Build is not installed on the system, then the rule must definitely be there.

A way around is to clear the rule toolset.using in build/config.jam after configure has be run. Another more permanent way is to add an empty file called user-config.jam to your home directory.

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: mCRL2 libraries cannot be found

With a shared build of the toolset, the dynamic libraries are not found at runtime. This can be solved by setting the LD_LIBRARY_PATH environment variable such that it includes the directory where the mCRL2 library (libmcrl2.so) is installed. This is a workaround, the current development version of the toolset does not need this.

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.

Windows (MinGW): installation uses wrong directory

Please use Windows-style paths instead of Unix-style paths. Also, use slashes (instead of a backslashes) for separating directories and use quotes if the path contains spaces, e.g. --prefix='C:/program files/mcrl2'.

Windows (MinGW): compiling or linking against wxWidgets fails

When wxWidgets was found by configure but the path returned by wx-config --prefix has a strange shape (e.g. /C/wxWidgets) then wxWidgets was configured and built with a prefix that is not understood by the shell. It is the same problem as above but for wxWidgets.

Toolset compilation takes a long time

Currently we do not have a solution to this problem. Please see the Trac ticket for more information.

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 compile 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.

---

lpsxsim