Catch a cat with TLA +

Formal methods are considered an effective, but unreasonably complex way to ensure software reliability. The tools used for this differ significantly from those familiar to the programmer. This article is written to lower the threshold for joining this toolkit. I will use the model checking system not for solving difficultly formulated tasks of software specifications, but for solving a puzzle that is understandable even to schoolchildren.



You are in a direct corridor with seven rooms on one side. In one of them is a cat. In one step, you can look into one of the rooms, if there is a cat, he is caught. As soon as the door closes, the cat will move into one of the neighboring rooms to the one in which he was. The task is to catch the cat.

TLA + and temporal logic

There are many tools that can solve such problems. Often in such cases, SMT-solvers are used. As a rule, such systems use the usual predicate logic and expressing the sequence of actions is quite complicated (you have to use something like an array, which is not very convenient to work with). In TLA + , temporal logic is used, which allows using the state of the system in one statement both at the current and at the next step.

CatDistr' = CatDistr \ {n}
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

This condition states that the set of rooms in which the cat can be located after checking the room n coincides with the set of rooms where n was taken from (if the cat was there, he is caught and there is nothing more to do).



In imperative programming languages, this roughly corresponds to assigning a variable a new value, calculated from the old one.

A bit about sets

As you understand, the position of the cat is modeled by a variable with the set of all possible rooms, and not a specific room, as it would be in a simulation system. Using the set of possible values ​​instead of a specific value is a frequently used technique in formal methods, which causes difficulty for novice programmers. Therefore, I chose a task where the use of sets is appropriate.

Program Structure in TLA +

In the simplest case, the program consists of declarations and statements (predicates) describing the initial state, the relationship between the current and next state, and the invariant that must be executed in all available states. Auxiliary predicates may also be present. Predicates can be parameterized.

 ---- MODULE cat ------------------------------------------------------------- EXTENDS Integers CONSTANTS Doors VARIABLES CatDistr, LastDoor Init == /\ CatDistr = 0..Doors /\ LastDoor = -1 OpenDoor(n) == /\ CatDistr' = 0..Doors \intersect UNION { {x-1, x+1} : x \in CatDistr \ {n} } /\ LastDoor' = n Next == \E door \in 0..Doors : OpenDoor(door) CatWalk == CatDistr /= {} =============================================================================
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

The first and last lines are the syntax features of the module declaration.



== means "equal by definition", while a single = is exactly the equality of the calculated values ​​of the expressions.



Doors is a model constant, it will need to be set in the configuration file.

CatDistr - the distribution of the cat in rooms.



The LastDoor variable, the last checked room, is entered for readability of program output. For large models, such variables can significantly slow down the program by increasing the number of analyzed states (since the state now contains a history of how it arose and the same states created in different ways will now be different).



The predicate Init describes the initial state (0..Doors is the set of all rooms). OpenDoor (n) describes what happens when you open the door to room n (in the worst case, the cat is not there - otherwise we caught him).



The Next predicate looks a little strange - there is a room to look into. The fact is that the existence of something means that TLA + does not know which room we will look into; therefore, it will check the correctness of the invariant in all cases.



It would be more clear to write

 Next == OpenDoor(0) \/ OpenDoor(1) \/ ... \/ OpenDoor(Doors)
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

but then our code will work only with a fixed number of rooms, and it’s better to make it parameterized.



And finally, the CatWalk invariant - a lot of rooms where the cat may not be empty. Violation of the invariant means that the cat was caught, wherever it was originally. When verifying the specification, violation of the invariant means an error, but we are not using the tool for its intended purpose and the “error” found means solving the problem.

Model configuration

 CONSTANTS Doors = 6 INIT Init NEXT Next INVARIANT CatWalk
      
      

        
        
        
      

    
        
        
        
      
      

        
        
        
      

    
     

Everything is simple here - we indicated the number of rooms, the initial conditions, the conditions for the change of state, and the invariant under test.



The model is launched from the command line tlc2 -config cat.cfg cat.tla .



TLA + has an advanced GUI launched by the tla-toolbox team. Unfortunately, he does not understand .cfg files and model parameters will need to be configured through the menu.

Conclusion

In this task, everything turned out pretty simple. Of course, practically significant cases of applying formal methods will require much more voluminous models and the use of various language constructions. But I hope that solving such puzzles will provide a simple and not boring way to implement formal methods in work projects.



→ The task was found here



Just in case, a simple program for interactive solution verification . Materials for the study of TLA + . Another model checking system, Alloy, is described here .