https://habr.com/en/company/waves/blog/462397/

• Waves corporate blog
• Programming
• System Analysis and Design
• Mathematics
• Logic games

Many programmers struggle when using formal methods to solve problems within their programs, as those methods, while effective, can be unreasonably complex. To understand why this happens, let’s use the model checking method to solve a relatively easy puzzle:

Conditions

You’re in a hallway with seven doors on one side leading to seven rooms. A cat is hiding in one of these rooms. Your task is to catch the cat. Opening a door takes one step. If you guess the correct door, you catch the cat. If you do not guess the correct door, the cat runs to the next room.

TLA+ and temporal logic

Some tools can solve problems like this. For example, SMT solvers, which are used frequently in these cases, use predicate logic to solve the problem, but that requires using an array, which is inconvenient for programmers and often results in an unnecessarily complex sequence of actions. TLA+, on the other hand, uses temporal logic, which allows a program to use the state of the system both at the current and next step in one statement.

CatDistr' = CatDistr \ {n}

This condition states that after checking behind door N, the number of doors where the cat can be located, coincides with the set of rooms where N was taken from. (If the cat was behind door N, of course, he’s been caught.)

In an imperative programming language, this creates a new variable calculated from the old one.

About sets

The cat’s position is determined by a variable within the set of all possible rooms, rather than specific room as in a simulation modeling system. Formal methods of programming take into account the plurality of possible values, instead of the current value. This is often too complex for beginning developers, so simplifying this system would help those developers work more quickly.

Structure of program in TLA+

The program consists of declarations and statements (predictors), which describe:

• The initial state
• The link between actual states
• The next state
• An invariant that runs in all available states.

There may be also auxiliary predicates (e.g. parameters) involved.

---- 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 /= {}

=============================================================================

In that example:

• The first and last lines declare that this is a source module.
• == means ‘equally by definition’.
• = means the calculated expression values are equal
• Doors is a constant set in the configuration file.
• CatDistr determines the room in which the cat is located.
• The LastDoor variable, which represents the last checked room, conveniently reads the output of the program. For big models, such variables could slow down the program workflow and increase the number of states that need to be analyzed. In this model, however, the state now contains history of which doors were opened. Thus, equal states created in different ways are now different.
• The Init predictor describes the initial state of the program — in this case, no doors have been opened yet.
• OpenDoor(n) describes what happens when door n is opened — either you caught the cat, or you didn’t.
• The Next predictor exists because TLA+ does not know in which room we might enter next, so it will check to see if invariants are correct in each case.
  
  Here is a more clear variant:
  
  

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

  
  In this case, the code works with a fixed number of rooms, making the code parameterized.
• Finally, the CatWalk invariant determines where the cat is hiding. An invariant breach means that the cat was caught wherever he hid. When verifying a specification, an invariant breach is an error, but since we are not using the tool for its intended purpose, getting an error in this case means solving the problem.

Model configuration

CONSTANTS
  Doors = 6

INIT Init
NEXT Next

INVARIANT CatWalk

This configuration includes the initial condition, the number of rooms, the conditions for a state change, and a verifiable test.

You can run this model from the command line using this command:
tlc2 -config cat.cfg cat.tla.

TLA+ has an advanced GUI and is launched by tla-toolbox command. Unfortunately, it does not understand .cfg files, so the model parameters must be configured through the menu.

Conclusion

Creating this particular program was fairly simple, but in many cases, applying formal methods will require much larger models and the use of various language constructions. We hope that solving simpler puzzles such as this will provide an easy and interesting way to apply formal methods the work projects.

• A simple program for interactive solution verification can be found here.
• Learn more about TLA+ here.