CSE308 (formally CSC_3S008_EP) - Tutorial 1: Modeling and Transition Systems

Setup

Setting up your environment.

1. You need to install the python packages contained in the requirements.txt file with pip:

   $ cd src
   $ pip install -r requirements.txt

   In case you have conflicts installing the packages versions, you can try with a python environment (or with anaconda).

   Download the graphviz library from here. We use graphviz to get a graphical representation of the transition systems.

   IMPORTANT: Get this done right away, you’ll need the same setup for the remaining tutorials.

2. Download and extract the files of the tutorial CSE308-TD1-1-handin.zip. You’ll find the folder called CSE308-TD1-1-handin.

Deadline and evaluation

Deadline.

The deadline for submitting the exercise to obtain a full grade is on Friday March 28 at 23:59.

You can submit your work after that deadline has passed but you will receive only 50% of the total grade (NOTE: I will evaluate only your last submission).

Evaluation.

You will receive 20 points, distributed as follows:

• Implementation of async_product (without synchronizations): 4
• SV transition system: 4
• Adding synchronizations to async_product: 2
• Implementation of check_invar without counter-example generation: 7
• Ccounter-example generation for check_invar: 3

Transition Systems

In this and in the following tutorials you will implement and experiment with the algorithm we learn in class. Today you will work with a data structure for representingß transition systems.

Concrete Syntax

You will be able to write transition systems with a concrete syntax (e.g., writing the system in a file). For example, consider the following transition system \(P_1\):

The transition system represents a process accessing a critical section. You can write the transition system with the following syntax:

states : 1,2,3;
init : 1;
actions : tau1,IN1,OUT1;
tr : (1, tau1, 2), (2, IN1, 3), (3, OUT1, 1);
ap : critical1;
labels : (3, (critical1));

In the above, states is a list of states (a state is either an integeror a tuple of states), actions is a list of identifiers (strings of letters and numbers starting with a letter), ap is a list of identifiers. init is a subset of the set of states, tr is a list of transitions and labels is a list of tuple assigning to a state a set of atomic propositions.

Transition system: data structure

The transition system data structure TS is is in src/mc308/auto/ts.py. First, take a look at the types used in the transition systems:

class StateTuple(tuple):
    """ Tuples of states are useful to represent products """
    def __new__(self, *args : int | StateTuple):
        return tuple.__new__(StateTuple, args)

State =  int | StateTuple
Action = NewType('Action', str)
Trans = Tuple[State,Action,State]

Observe that:

• a state is an integer or a tuple of integers
• actions are strings
• transitions are tuples of 3 elements, a state, an action, and a state.

So, the transition system data structure corresponds to the formalization you saw in class and it has:

• A set of states (states : Set[State])
• A set of initial states (states : Set[State])
• A set of actions (actions : Set[Actions])
• A set of transitions (tr : Set[Trans]). A transition is, for example, (1, "tau1", 2).
• A set of atomic propositions (ap : Set[BoolFormula]). While BoolFormula is a type representing a Boolean formula (more on this later), each atomic proposition is just a Boolean variable.
• A labeling from states to set of atomic propositions (labels : Mapping[State, Set[BoolFormula]]).

You can get a transition system parsing a string with the concrete syntax we saw above:

from mc308.auto.ts import TS
from mc308.parsers.ts_parser import TSParser

input_data = """
states : 1,2,3;
init : 1;
actions : tau1,IN1,OUT1;
tr : (1, tau1, 2), (2, IN1, 3), (3, OUT1, 1);
ap : critical1;
"""

p = TSParser()
ts = p.parse(input_data)

And you can construct the same transition system directly in python:

# Declare a Boolean variable
critical = Symbol("critical")

ts = TS([1,2,3],
        ["tau1","IN1","OUT1"],
        [(1, "tau1", 2), (2, "IN1", 3), (3, "OUT1", 1)],
        [critical],
        {3 : [critical]})

You can also print your transition system in an image as follows:

from mc308.auto.visualization import to_png, ts_to_dot

dot = ts_to_dot(ts)
with open("/tmp/output.png", "w") as f:
  to_png(dot, f)

Use this section as a reference for working on the transition system, no exercises to do so far.

Compute the interleaving of two transition systems

Interleaving

We can model concurrent processes via transition systems. Consider the following two processes:

The two processes access a critical section when they are in the state 3 (they have the label critical).

First, write on paper the interleaving of the transition system \(P_1\) and \(P_2\) (\(P_1\ |||\ P_2\)). Note that for now the two transition systems do not synchronize.

You will work in the file src/mc308/td1.py and implement the function that computes the interleaving (or asynchronous product) of two transition systems:

def async_product(t1 : TS, t2 : TS) -> TS

For now, you can assume ts1 and ts2 do not synchronize any transition on common actions.

As usual, when writing your code, prefer clarirty to use hyper compact implementations (and kindly add some comments to help understanding your code).

How to try your code: look at the file src/td1_script.td. It contains the code to run your implementation on the two transition systems in the function:

def test_ex1()

The function:

• loads the two transition systems from file
• call the async_prod function
• creates a png of the result in p1_p2.png

You are free to print other things (e.g., in python, you can print the textual representation of the transition system ts, e.g., print(ts)).

IMPORTANT: Your implementation should work on different inputs (i.e., different transition systems) too. While there are no automatic tests, you can add more to feel more confident about your implementation.

Asynchronous Product with Message Passing

The asynchronous product \(P_1 \parallel P_2\) allows the two transition systems to enter the critical section together (that’s clearly bad…).

How can you fix the problem?

A solution to the problem is to block \(P_1\) to enter the critical section (executing the transition with the action \(IN_1\)) when \(P_2\) is in the critical section, and allowing \(P_1\) to enter the section only after \(P_2\) left the section (executing the transition with action \(OUT_2\)).

A similar reasoning applies switching the role of \(P_1\) and \(P_2\).

You can achieve this result writing a new transition system \(SV\) modeling a shared variable that:

• synchronize with \(P_1\) on the actions \(IN_1\) and \(OUT_1\).
• synchronize with \(P_2\) on the actions \(IN_2\) and \(OUT_2\).
• allows \(P_1\) (resp. \(P_2\)) to enter the critical section only if \(P_2\) (resp. \(P_1\)) is not in the critical section itself.

Clearly, you want the composed system \((P_1 \parallel P_2) \parallel SV\) to:

• still allow \(P_1\) and \(P_2\) to acquire the critical section; and
• ensure the mutual exclusion on the critical section.

Write on paper the asynchronous product \((P_1 \parallel P_2) \parallel SV\). This is the message passing operations we saw in class, where transitions labeled with an action in the common set must be taken “together” in both transition systems.

Change your implementation of async_product to consider the synchronizations (i.e., common labels). Test your implementation on the example above.

You can test the example above with test_ex2.

Invariant Checking Algorithm

Implement the invariant checking algorithm in the function:

def check_invar(ts : TS, invar : BoolFormula) -> Tuple[bool, Optional[FinitePath]]:

always in the src/mc308/td1.py file.

The function:

• takes as input a transition system ts and a Boolean formula `invar; and
• returns a tuple where:

  • the first element is true if and only if invar is an invariant of the tranition system ts.

  • the second element is a path in ts starting in an initial state and ending in a state that does not satisfy invar (i.e., \(s \not \models invar\)).

    For your first implementation, your function can always return None for the second element.

You can try the check_invar function on the transition system \(P_1 \parallel P_2 \parallel SV\) and the following invariant properties:

• \(\neg (critical_1 \land critical_2)\)
• \(\neg critical_1\)
• \(\neg critical_2\)

The function test_ex3 does exaclty that.

Aside: Working with Boolean formulas

invar is a Boolean formula.

We use the python package PySMT for representing Boolean formulas. For now, just understand how you can:

• declare a Boolean variable

from pysmt.shortcuts import Symbol

a = Symbol("var") # declare a Boolean variable named var
print(a)

• Build a Boolean expression:

from pysmt.shortcuts import Symbol, Not,And,Or,Implies,Iff

a,b,c = [Symbol(n) for n in ['a','b','c']]
# formula (a & b) | (!c)
f = Or(And(a,b), Not(c))

print(f)

And you can check if the label for a state s in a transition system satisfies a formula \(\psi\) (i.e., L(s) $) using the function eval_state in the TS class.

Building a Counter-example

Implement the construction of the counter-example for the function check_invar.

Submission

You will submit the file td1.py containing the (final) implementation of async_product and check_invar, and the file sv.ts containing your solution for the “shared variable” transition system.