secretIt seems to be popular to write Fowler’s DSL in all languages. I follow this idea and start a series of posts on TLA+ with Fowlers state-machine example coded in TLA+. TLA+ is a specification language developed by Leslie Lamport.  TLA+ is based on Temporal Logic of Actions, which combines logic of actions (denoting the state change of the system) with temporal operators. This specification language allows reasoning on dicrete systems and is quite powerful. It is even more intersting, that the language is equiped with a set of tools. The TLA+ Tools include a Syntax Analyzer (SANY), a Simulator with Model Checker (TLC) and a pretty printer, for creating LaTeX-style representation of the source. The tools are implemented in Java and are published under MS-Research license. The source code of the tools is also available. Since TLA+ is developed by the father of LaTeX, its ASCII representation looks very similar to LaTeX, and is convenient for the input.

(* ************************************ *)
(* Controller of the secret compartment *)
(* of Mrs. H, who loves secrets!        *)
(* Following the example of M. Fowler,  *)
(* which can be found at:               *)
(* http://martinfowler.com/             *)
(* ************************************ *)
------------- MODULE fowler --------------
(* ************************************ *)
(* Variables                            *)
(* ************************************ *)
VARIABLE 
  state, \* the state for display, only 
         \* to be compliant with  Fowler
  light, \* state of the light
  draw,  \* state of the draw
  panel, \* state of the secret panel
  door   \* state of the entry door

TypeInv == 
(* ************************************ *)
(* Type invariance                      *)
(* ************************************ *)
  /\ state \in { "idle", 
                 "active", 
                 "waitingForDraw", 
                 "waitingForLight", 
                 "unlockedPanel" }
  /\ light \in { "on", "off" }
  /\ draw \in { "opened", "closed" }
  /\ door \in { "locked", "unlocked"}
  /\ panel \in { "locked", "unlocked" }
 
Init == 
(* ************************************ *)
(* Initial state                        *)
(* ************************************ *)
  /\ state = "idle"
  /\ light = "off"
  /\ draw  = "closed"
  /\ door  = "unlocked"
  /\ panel = "locked"
------------------------------------------  
(* ************************************ *)
(* Actions                              *)
(* Note that the state variable is not  *)
(* used for the determination of the    *)
(* actual state, but only for display.  *)
(* This shows that this variable        *)
(* is not required in TLA+              *)
(* ************************************ *)
  
CloseDoor == 
(* ************************************ *)
(* Closes the door, to activate         *)
(* ************************************ *)
  /\ door = "unlocked"
  /\ door' = "locked"
  /\ state' = "active"
  /\ UNCHANGED << panel, light, draw >>
  
LightOn == 
(* ************************************ *)
(* Switch on the light, if the draw is  *)
(* opened, this opens the secret panel  *)
(* ************************************ *)
  /\ light = "off"
  /\ light' = "on"
  /\ IF draw = "opened" THEN 
       /\ state' = "unlockedPanel"
	   /\ panel' = "unlocked"
	   /\ door' = "locked"
	 ELSE 
	   /\ state' = "waitingForDraw"
	   /\ UNCHANGED << panel, door >>
  /\ UNCHANGED << draw >>

OpenDraw ==
(* ************************************ *)
(* Open the draw, if the light is on,   *)
(* this opens the secret panel          *)
(* ************************************ *)
  /\ draw = "closed"
  /\ draw' = "opened"
  /\ IF light = "on" THEN 
       /\ state' = "unlockedPanel"
	   /\ panel' = "unlocked"
	   /\ door' = "locked"
	 ELSE 
	   /\ state' = "waitingForLight"
	   /\ UNCHANGED << panel, door >>
  /\ UNCHANGED << light >>

ClosePanel ==
(* ************************************ *)
(* Closes the secret panel and move the *)
(* system to initial state              *)
(* ************************************ *)
  /\ panel = "unlocked"
  /\ panel' = "locked"
  /\ light' = "off"
  /\ draw' = "closed"
  /\ door' = "unlocked"
  /\ state' = "idle"
------------------------------------------
Next == 
(* ************************************ *)
(* All possible actions                 *)
(* ***********************************  *)
  \/ CloseDoor 
  \/ LightOn 
  \/ OpenDraw 
  \/ ClosePanel

Spec == Init /\ [][Next]_<< panel, light, 
  draw, door, state >>

THEOREM Spec => []TypeInv

Inv == 
(* ************************************ *)
(* The panel is never unlocked          *)
(* by opened door                       *)
(* ************************************ *)
  \/ panel = "unlocked" => door = "locked"  
  \/ door = "unlocked" => panel = "locked" 
==========================================

In order to run a model checker, the configuration file fowler.cfg needs to be created. It says which part of the model is the specification, and what should be checked. In the example above, the specification action is called Spec and states, that if the Init action is executed, the Next action can always be executed by allowing stuttering steps by changing values of the variables panel, light, draw, door and state. The actual property we want to check is the fact, that the compartment is really safe, which means that the secret panel can be unlocked if and only if the door is closed. This is stated in the property Inv which has to be an invariant property of the system.

SPECIFICATION   Spec
INVARIANT       Inv

Running TLC on this specification, with configuration file provided above produced the following output:

TLC2 Version 2.01 of February 23, 2008
Model-checking
Parsing file fowler.tla
Semantic processing of module fowler
Finished computing initial states: 1 distinct state generated.
Model checking completed. No error has been found.
Estimates of the probability that TLC did not check all reachable states
because two distinct states had the same fingerprint:
calculated (optimistic):  2.927345865710862E-18
based on the actual fingerprints:  1.2569902552401487E-14
15 states generated, 9 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 3.

This means, that it reached all states with very high probability and checked in every state the required property.
The compartment of Martin is safe! Modelchecked by TLC.

Tags: , , , , ,