User manual/squadt

From MCRL2

User manual

Tool manual pages chi2mcrl2 diagraphica formcheck grapemcrl2 lps2lts lps2pbes lps2torx lpsactionrename lpsbinary lpsbisim2pbes lpsconfcheck lpsconstelm lpsinfo lpsinvelm lpsparelm lpsparunfold lpspp lpsrealelm lpsrewr lpssim lpssumelm lpssuminst lpsuntime lpsxsim lts2lps ltscompare ltsconvert ltsgraph ltsinfo ltsmin ltsview lysa2mcrl2 mcrl22lps mcrl2-gui mcrl2i pbesinst pbes2bool pbesconstelm pbesinfo pbesparelm pbespareqelm pbespgsolve pbespp pbesrewr pnml2mcrl2 squadt tbf2lps tracepp txt2lps txt2pbes

Contents

Interactive integration of software tools

Contents 1 Synopsis 2 Short description 3 Options 4 Detailed description 4.1 Overview 4.2 Projects 4.3 Graphical User Interface 4.3.1 Data view 4.3.2 Activity view 4.4 Editing 5 Author 6 Bug reporting

Synopsis

squadt [OPTION]... [PATH]

Short description

By default SQuADT starts and draws the graphical user interface, after which it waits for user interaction. Alternatively, when PATH is provided, it tries to open an existing project in PATH.

Options

OPTION can be any of the following:

-c, --create

create new project in PATH

-pPORT, --port=PORT

listen on TCP port number PORT

Standard options:

-q, --quiet

do not display warning messages

-v, --verbose

display short intermediate messages

-d, --debug

display detailed intermediate messages

-h, --help

display help message

--version

display version information

Detailed description

Overview

The SQuADT application provides a framework for tool integration. In the current version it is only possible to run tools that are present on the same machine that SQuADT is running on. The current setup does just this but in the future it should not matter on what machine the tools are running, as long as a tool can be started and can connect to SQuADT.

A custom build protocol based on XML-formatted messages is used for communication between tools and the SQuADT application across a TCP connection. This should allow almost any tool written in almost any programming language to connect and operate within this framework.

Projects

All operations occur within a project context, which is used by the system to collect and store information that can be used to automate certain tasks for the user. Creation of a new project consists of choosing a separate directory called project store. Associated with the project are all files that are assigned to it by the user or that are generated as part of tool operation.

The SQuADT application manages the contents of the project store. Files added to a project by the user are copied to this directory and erased when they are removed from the project. As part of the protocol the tool communicates what files have been used as input and what files have been produced during a tool run. The next section that discusses the data view tells how files can become part of a project.

Graphical User Interface

The main screen is split into two views, a view on the data in the project, and an activity view.

Data view

The data view shows sources of data and their main interdependencies. Below is a screenshot that shows the data view in SQuADT. Every icon represents a source of data, meaning a single file in the store. The colours indicate status. For instance a tool can be actively generating a file, or data in a file can be corrupted because a tool crashed while it was generating the data. To give the user a clue as to what is happening and what has happened the status is interactively updated while tools run in the background.

It is important to realise that the view only displays files in the project store that have been added to the project by the user, or files that can be created by running tools on other files in the project. Copying files to and from the project store has no effect, the system will ignore them or a tool may overwrite them if file names collide. Also note that not every object in the data view needs to actually correspond to a file in the project store. The data view (partly) visualises dependencies among data sources. It shows that the system `knows' what tools it must apply to what input in order to obtain each data object. The colours in the data view should be interpreted as follows:

 

file contents is authentic (added by the user), so it is always up-to-date

 

file contents is derived from other data and up-to-date

 

file contents is derived from other data, present in the project store but not up-to-date with respect to the data sources it depends on

 

file contents is derived from other data and is not available in the project store or is considered corrupt

 

file contents is being generated

As hinted at before here are two ways in which a file can become part of a project. The first is when a user manually adds it to a project. These files are called original or authentic because once lost they cannot be recreated without user intervention. Adding an original file is performed by selecting the appropriate option in the `Project' menu, as illustrated below.

The second way that files become part of a project is when they are produced by running a tool from the project store. The tool may require input from other files in the project. Such files are called the (input) dependencies. It is assumed that SQuADT is aware of all input dependencies in a project and one of its tasks is to make sure that all non-authentic files are up-to-date with respect to the files on which they depend (recursively). This means that changes propagate inversely across dependencies.

Note that there is an important restriction with regard to interfile dependencies. A tool may not depend for input on it's own output, or any file derived from it. Or equivalently cycles are not allowed in the dependency graph. The consequence is that there is only one way to generate each derived data source. This ensures that if all tools can process input and produce output in a finite amount of time, then all files in a project can be reproduced from the authentic files in a finite amount of time as well.

The data view is not just a passive visualisation of data in the project store. In addition it also functions as an interface for managing the project store. The following picture shows the operations that can be performed on a single file.

The context menu can be obtained by activating (right/double clicking) the object in the data view. From top to bottom. Rename can be used to edit the name of an object (and the associated file). Remove deletes the object and every object that depends on it (transitive-closure). Refresh brings the object and all objects it depends on in up-to-date status (transitive-closure). Configure starts a tool and reconfigures the tool that was used to generate the object. Clean removes the associated file from the project store, but retains the information on how it can be produced by running tools. The menu options between the separators are categories that characterise functionality of the set of known tools that take as (main) input a file with a type that corresponds with the type of the selected object. Finally the menu-option details shows a dialog that contains details on how the file was created (or how it can be recreated).

Activity view

The activity view shows activity of running tools as well as tools that might have already finished. Each tool instance is associated to a sub-window in the activity view associated. Such a window is called a `tool display' and is hidden by default. The tool display is not visible unless a tool activates it in some way.

The tool display represents a specific task that is being performed or has been performed. The task is performed by a single tool that is running in the background or has terminated already. Using the tool display the user can configure the tool to perform a task or see task progress information. The tool display is a communication channel between a tool instance and the user. For richer user-interaction the tool can also communicate with a user through its own graphical user interface.

Editing

Files can be manipulated by all kinds of tools that connected to SQuADT. An important class of useful tools namely editors are not available. To still be able to use such tools it is possible to invoke custom edit action on any file in a project. The inner workings are as follows. A command that performs the desired operation is associated with a file type. The command is executed in the default shell when the edit action is invoked.

The preferences menu gives access to the list of type/command associations. The list contains the types that are known to SQuADT after it's initialisation. The types are gathered by querying known tools. If initialisation fails for some tools then some types may not be in the list. It is possible to manually add a type/command pair, or to edit existing pairs. As an example the following command can be used to pretty print an mCRL2 linear process specification (LPS) and view the result in the editor vim.

/bin/sh -c '/usr/bin/lpspp $ | /usr/bin/gvim -'

The command looks very complex for technical reasons, the goal is actually to execute '/usr/bin/lpspp $ | /usr/bin/gvim'. The shell (/bin/sh) is used to set up communication channels between the lpspp and programs gvim. Notice that the $ will be replaced by the target of the edit operation. For a file abp.lps, the result will look as follows:

/bin/sh -c '/usr/bin/lpspp abp.lps | /usr/bin/gvim -'

For this mechanism to work as expected it is very important that the type of a file is known to SQuADT. This should be the case for any file generated by a tool. In this case the type is communicated as part of the message that a tool sends to inform SQuADT about the existence of the file. Of course a tool may communicate a bogus type and SQuADT will never know about it (considered a bug in the tool). For files added to a project by the user the type is guessed from the name of the file.

Author

Written by Jeroen van der Wulp.

Bug reporting

Report bugs at our issue tracking system.

---

pnml2mcrl2

tbf2lps