Formal Methods – A Learning Environment

par4fun is a tool supporting concurrency from Chapter 8 of the book Formal Methods – An Appetizer.

Browser Compatibility

The tool uses a responsive design and can be used on any device with a modern browser. The tool has been developed and tested in Google Chrome v60. The online version of the tool has also been tested in Firefox v49, Opera v46, Safari v10, and Internet Explorer v11.

About

The core functionality is written in F# and then converted to JavaScript using Fable.

Developed by Kasper Laursen, Hanne Riis Nielson and Mike Castro Lundin, based on the specification developed by Hanne Riis Nielson and Flemming Nielson.

This software is protected under the Simplified BSD License and the Intellectual Property Rights of the Technical University of Denmark.

Bugs and suggestions

Please report all bugs and suggestions to post@formalmethods.dk.

Download

This tool is compiled to javascript, and therefore only requires a browser to run. Download the tool for offline usage.

Download Formal Methods – A Learning Environment

Shared Variables

Explore how the memory changes, upon execution of the actions. Recall that if more guards are satisfied then it is non-deterministic which action to take.

When using the Show Trace, non-deterministic choices will be shown in the first column as , and if clicked the trace will be "reset" from that configuration.

When using the Show Resulting Configurations, all non-deterministic choices will be explored, until it reaches the number of steps, gets stuck or terminates. A short summary of the final configurations is found at the end. Warning If the input code is highly non-deterministic, and the number of steps is high, the tree of possible end-configurations will grow big (and therefore long execution).

For both outputs all non-terminated (or non-stuck) configuration can be extended with 1-1000 steps.

Recall that the shared variables syntax does not include channels c or the loop CG pool construct.

Asynchronous Communication

Explore how the memory changes, upon execution of the actions. Recall that if more guards are satisfied then it is non-deterministic which action to take.

When using the Show Trace, non-deterministic choices will be shown in the first column as , and if clicked the trace will be "reset" from that configuration.

When using the Show Resulting Configurations, all non-deterministic choices will be explored, until it reaches the number of steps, gets stuck or terminates. A short summary of the final configurations is found at the end. Warning If the input code is highly non-deterministic, and the number of steps is high, the tree of possible end-configurations will grow big (and therefore long execution).

For both outputs all non-terminated (or non-stuck) configuration can be extended with 1-1000 steps.

Recall that the asynchronous communication syntax includes channels, which are stored in a buffer; and the loop CG pool construct.

Synchronous Communication

Explore how the memory changes, upon execution of the actions. Recall that if more guards are satisfied then it is non-deterministic which action to take.

When using the Show Trace, non-deterministic choices will be shown in the first column as , and if clicked the trace will be "reset" from that configuration.

When using the Show Resulting Configurations, all non-deterministic choices will be explored, until it reaches the number of steps, gets stuck or terminates. A short summary of the final configurations is found at the end. Warning If the input code is highly non-deterministic, and the number of steps is high, the tree of possible end-configurations will grow big (and therefore long execution).

For both outputs all non-terminated (or non-stuck) configuration can be extended with 1-1000 steps.

Recall that the synchronous communication syntax includes channels, but does not use buffers.