Handling States in lisb
Currently (since quite a while), I am experimenting with a nice way to represent states (of a B machine, for example) in lisb / Clojure. I think at this point I am close enough to something I like. Things might still change, but probably the ideas I outline below should hold (unless there is a good reason it cannot be implemented nicely).
Rationale
Part of my research interest is to bring formal methods closer to practitioners. This means, they must be accessible for programmers and must not exist on some isolated island groups made up from the specification language and some tools.
The ProB Java API offers a lot of possibilities here. During implementing it in lisb, i.e., from a Clojure point of view, it is a horrible object-oriented mess.
The essence, I think, is that a state should map a variable to a value. In lisb, this value should be something that a Clojure developer can work with; it should be Clojure data or a proper representation if it cannot be translated (e.g., infinite sets).
Usage
Loading a state space
The State Space object in the ProB Java API is, more or less, the connection to ProB's animator process. It is the context in which states live and are susceptible to the operations defined in the B machine.
user=> (def state-space (state-space! (b->ast (slurp (clojure.java.io/resource "machines/b/simple/Lift.mch")))))
user=> (def state-space2 (state-space! (b->ast (slurp (clojure.java.io/resource "machines/b/CAN_BUS_tlc.mch")))))
Getting started
The state space gives us a reference to a special root state. In this state, constants and variables are not initialised yet. ProB has virtual operations to (a) setup constants (but only if there is at least one constant) and (b) to initialise the state variables.
user=> (root-state state-space)
{:etage :prob/uninitialised, :op/$initialise_machine ...}
user=> (root-state state-space2)
{:T3_evaluated :prob/uninitialised, :BUSpriority :prob/uninitialised, :T2_mode :prob/uninitialised, :T2_timer :prob/uninitialised, :T1_timer :prob/uninitialised, :NATSET :prob/uninitialised, :T3_enabled :prob/uninitialised, :BUSwrite :prob/uninitialised, :T2_readpriority :prob/uninitialised, :T3_readvalue :prob/uninitialised, :T3_readpriority :prob/uninitialised, :T2_readvalue :prob/uninitialised, :T2v :prob/uninitialised, :T1_writevalue :prob/uninitialised, :T2_writevalue :prob/uninitialised, :BUSvalue :prob/uninitialised, :T3_state :prob/uninitialised, :T2_state :prob/uninitialised, :T1_state :prob/uninitialised, :op/$setup_constants ...}
We see the basic representation in lisb here already:
It is a map; and it is mapping identifiers to values.
Further, it maps available operations to ... - a something that is not known yet!
(We could put the next state there, but we do not want (infinite) nesting of states in the print.)
Step-by-step: Getting the next state
We can actually access the operations and get the successor state.
user=> (def lift-init (get (root-state state-space) :op/$initialise_machine))
user=> lift-init
{:curfloor 4, :op/inc ..., :op/dec ...}
This can be repeated as much as you want:
user=> (get-in lift-init [:op/inc :op/inc :op/inc])
{:curfloor 7, :op/inc ..., :op/dec ...}
You basically have ProB's animator at your hands now.
Setting up constants
Setting up constants is an extra operation that is executed before initialising the state variables, for example:
user=> (def state (get-in (root-state state-space2) [:op/$setup_constants :op/$initialise_machine]))
user=> state
{:T3_evaluated true, :BUSpriority 0, :T2_mode :T2MODE_SENSE, :T2_timer 3, :T1_timer 2, :NATSET #{0 1 4 3 2 5}, :T3_enabled true, :BUSwrite #{{:tag :maplet, :elems (0 0)}}, :T2_readpriority 0, :T3_readvalue 0, :T3_readpriority 0, :T2_readvalue 0, :T2v 0, :T1_writevalue 0, :T2_writevalue 0, :BUSvalue 0, :T3_state :T3_READY, :T2_state :T2_EN, :T1_state :T1_EN, [:op/Update {"pmax" "0"}] ...}
Parameterized Operations
The last map entry above was [:op/Update {"pmax" "0"}] ....
(Note for you and me: this might and should change to a keyword and a proper Clojure value.)
This is because the operation takes a parameter (in B: Update(pmax) = ...).
0 is a valid (and the only) value for the parameter pmax that satisfies its constraints in the model.
We have two possibilities to access it. First, we can access it exactly as printed, specifying all parameters (in this instance, one):
user=> (get state [op/Update {:pmax 0}])
;; long print of an entire state again
The second possibility is to just state the operation:
user=> (get state op/Update)
;; long print of an entire state again
This will choose any solution satisfying the parameters. In this case, since there only is one solution, it will execute the same transition as above.
Interacting with a state
Accessing the state
We can access a state variable simply as one would expect:
user=> (get lift-init :curfloor)
4
Modifying the state
You can get a new state by modifying the map.
user=> (assoc lift-init :curfloor 42)
{:curfloor 42, :op/inc ..., :op/dec ...}
update etc. will work as well.
Note: associng many variables at once might be inefficient.
For each individual assoc of a single variable,
we ask ProB to add a virtual transition from the root state
to the modified state (satisfying that all variables match the specified ones).
The, the new state is returned (and if there are more variables to be assoc'd, this is repeated).
Creating a state out of thin air
Imagine, you already have all data. Like:
(def my-state-bindings {:curfloor 97})
You can get a state (via the same mechanism outlined above, but only one call to ProB) from this map:
user=> (to-state state-space my-state-bindings)
{:curfloor 97, :op/inc ..., :op/dec ...}
As you can see, you need the state space reference again. Remember what I told you earlier: It is the context that gives the variable binding data meaning (e.g., invariants, operations, ...).
No strings attached
One last thing:
The states you use in lisb implement APersistentMap.
Technically, you can assoc extra variables into it.
I have not tested this yet.
But, they are a bit more than a map. They have access to the State object of the ProB Java API as they capture it in their closure. If you need it for yourself (e.g., to get back to the state space), you can retrieve it from its metadata.