Using TLV

1. SMV Mutex

Translate the mutual-exclusion system mutex.spl from SPL to SMV. You should prepare a file mutex.smv containing your translation. You will further use this file in question 3. Note: It is normally easier to first translate SPL into FDS, and then FDS into SMV.

2. Proving partial correctness using TLV

Consider the pile.spl program. This program plays a game with a user. The game starts with a pile which contains 33 tokens. The user and computer take turns - with the user starting first. In each step the user or computer subtracts from 1 to 3 tokens from the pile. The player who is forced to take the last token loses the game.

You need to prove the program is partially correct, that is, upon termination the computer always wins. TLV will assist you in finding the inductive assertions. Start TLV with the pile.smv file, which is a ready-made translation of pile.spl to SMV.  Define an array C of cut-points, and array A of assertions. Use the following TLV utility command:

    chk_inv C, A, <number-of-cutpoint> ;

You can use this command interactively many times as you improve your assertions. It will either approve your assertion network to be inductive, or will provide a counter-example to assist you strengthening your assertions.

When done, place your cut-points + assertions + chk_inv invocation in a pile.tlv file.

3. Proving a property of a reactive system

We want to prove that the mutual-exclusion system in mutex.spl satisfies the property that P1 and P2 can never be in their critical section at the same time. If that property is satisfied, there cannot be a state reachable from the initial state, in which P1 and P2 are both in their critical section.

Write a TLV function called Inv in a file named inv.tlv, that takes a property as argument, and returns true if the system satisfies the property, and false otherwise.

Submission

Compress the all the files (mutex.smv, pile.tlv, inv.tlv)  into one zip-file and submit it using the submission system.