The UofO LOTOS Project

LMC User Manual

This text is an attempt at explaining the new features that have been to theLMC after Brahim's thesis... It also hopefully provides enlightenment on some obscure points. This document hopefully provides enough information for anyone willing to use LMC and having some basics knowledge of the CTL operators (see the thesis for explanations on this). It is the only user-oriented document related to the handling of symbolic values in LMC .

Inputs

To prove formulas, LMC needs the LTS of the specification you are working on. We have a tool allowing the expansion of a specification, it is Sela. So, in order to check formulas on a given specification is to run Sela on it. Sela has a lot of flags, the value of one of them is mandatory. It is the one indicating the detection method. Its value MUST be STRICT. The reason for this involves theoretical stuff which doesn't belong to this document. So, the first input to LMC is a symbolic tree generated by Sela with the detection of recursions set to STRICT. The limits on the size (depth and width) of the tree are specified at this stage and may affect the results of LMC .

The other input is obvious: it is the formula to check itself. Not much to say about this, except for the syntax which is provided at the end of this document.

Symbolic trees and LMC trees

To be able to actually perform the checking the first thing LMC does is to transform the symbolic tree generated by Sela in another tree called the LMC tree. This tree can be saved and used later for other proofs. The fact is that the LMC tree is what is actually used for the checking of formulas, not the symbolic tree.

NB: as soon as you load a LMC tree in memory the specification you were previously working on is no more available (even if it is the one the LMC tree has been derived from).

Infinity and Inconclusiveness

Some specifications have an infinite symbolic tree which, of course, cannot be computed (the limits in depth and width have been added to avoid explosion). Therefore, some formulas cannot be proven to be true (or false for that matter). This led Brahim to use a 3 states logic. The three possible results for a checking are therefore true , false and inconclusive . Let's see an example of an inconclusive result by considering the following specification:

clock[g](0)
where process clock[g](x:nat):noexit:=
	g !x; clock[g](succ(x))
      endproc

The resulting tree is obviously infinite. However, since Sela has a limit on the depth of the generated tree, the actual tree will be cut and the last edge will be replaced by a continue edge meaning that the tree has been cut because of the limits provided by the user.

If we want to check that the formula ag(g !*) holds, we cannot (more on the * later, just consider that !* matches any possible value). Indeed, there is a part of the tree that is unknown to the system (after the continue edge). Hence, there is no way, the LMC can conclude on the whole specification. However, the formula holds on the part of the tree it is aware of. The result is inconclusive .

Zero is the first

Not too much to say, just that the first node of the LMC tree (referred to as node 0) doesn't have any action (it exists for some theoretical requirement on the LMC tree). Therefore, checking the formula g is pretty dumb. Instead, checking ax(g) or ex(g) can be interesting.

Parentheses

The use of Parentheses is important since it affects the meaning of a formula to be evaluated. Parentheses also help clarify the order of evaluation of the operators involved.

Consider the following example:

buffer[in1, out]
where process buffer[in1, out]:noexit:=
	in1 ?x:bit; out !x; buffer[in1, out]
      endproc

The symbolic tree generated by Sela is finite because Sela detects the recursion corresponding to the recursive instantiation of the process buffer. The symbolic tree is equivalent to the original specification and therefore we can conclude that there won't be any inconclusive result (although the behavior is infinite). Anyway, let's consider we want to check the following formula:

ax(in1 !0) & ax(ax(out !1))

If we don't look close enough at it, we are tempted to conclude that this isfalse ... Of course, it is not and the computer invariably answers that this formula holds. Now, let's try something else:

ax(in1 !0 & ax(out !1))

This time, the answer is that the formula is false . Let's try to understand what is the difference between those two formulas. The first and most obvious answer is of course the position of the and operator. And indeed, that's what makes the whole difference.

In the first example, the checker is sitting at the node 0 and what the user asks it to do is:

Go to all the next nodes and check that each of them matches with in1 !0
Come back to the node 0
Go to all the next-next nodes and check that each of them matches with out !1

In the second example, the checker is sitting at the node 0 and the users give it the following orders:

Go to all the next nodes and check that each of them matches with in1 !0
From each of those nodes go to all the next nodes and check that each of them match with out !1

To put it another way, the problem is that with the first formula we consider two actions coming from different instantiations of the process buffer, whereas in the second they both come from the same. In the first formula, checking that in0 !1 and in1 ?x match is true if and only if we bind the value identifier x to 0. There is only one value identifier for each instantiation of the process buffer. Hence, in the second formula we first bind the value identifier to 0, then we try to match out !1 to out !x (with x bound to 0). That is not possible and the result is false . On the other hand, in the first formula we first bind x to 0 but we forget the corresponding instantiation of buffer (by coming back to the node 0 ) and subsequently the binding. So, when we reach the out !1 in the formula we try to match it with out !x (x being unbound at this point). The attempt is obviously successful and the result of the whole checking is that the formula holds.

Following the same line of reasoning, we can conclude that the formula

ax(in1 !0 & in1 !1)

doesn't hold although the formula

ax(in1 !0) & ax(in1 !1)

does.

The * value

This facility is mentioned in Brahim's thesis. The * matches with any value of any sort. We used in one of our previous examples to specify that all the actions offered by the spec were on gate

and had only one experiment. This was translated into the formula ag(g !*)

Symbolic values

That's probably the most important part of this document. The handling of symbolic values has been the core of the improvements added to the previous version of LMC . But before going any further, let's have a look at what a symbolic value is (for more detailed information, see the corresponding document). A symbolic value can be defined as a value we don't necessarily know. The only thing we know for sure about it is its name. As time passes, it may get a value. It also may be asked to fulfill some constraints (equations). Therefore a symbolic value can be defined as a triplet constituted of a name, a possible value (an actual value or a no value ) and a set of equations on this symbolic value.

Let's notice that symbolic values were first introduced in Sela. They are used to provide values at points where the user would have done it in a regular execution. If we consider our buffer example, Sela would have provided a symbolic value bit@1 at the in1 gate. And this very same symbolic value would have been offered to the environment on the gate out at the next action.

LMC uses the results of Sela. The introduction of symbolic values in the formulas to check was therefore the next logical step. Of course, this is not so simple as one would think at first sight. But first of all, let's give an example of the use of symbolic values in LMC formulas.

Let's keep out buffer example and let's try to check that whatever comes in will get out (as you probably noticed this very simple buffer is deterministic). This can be expressed by the formula:

ag(in1 !@1 --> af(out !@1))

In this formula, @1 is a symbolic value (the use of names of the form @<N> for symbolic values is mandatory).

Now, let's see the mechanisms involved in checking this formula on the symbolic tree. First of all we must find all the actions of the tree that match in1 !@1 (it is on the left part of an implication and the implication is always true when its left part is false ). There is only one such action, it is in1 !bit@1 . The two actions match if and only if @1 = bit@1 . This is a constraint added to the sets of equations associated to the two symbolic values @1 and bit@1 . Now, to prove the whole formula we must check that in all the futures ofin1 !bit@1 , there is an action that matches with out !@1 . Indeed, there is one, it is out !bit@1 which matches out !@1 if and only if @1 = bit@1 . This equation should be added to the sets of equations associated to the two symbolic values but is not because it is already there. We can conclude that the whole formula is true if and only if @1 = bit@1 and that's exactly the result we get.

What about trying symbolic values on the clock process? The formula we checked earlier could be specified without the * value but using a symbolic value instead. So, let's try to check that the following formula holds:

ag(g !@1)

Unfortunately, the result is that the formula doesn't hold. Strange, isn't it? Let's try to prove this formula step by step. What we are asked to do is to check that all the actions offered match with g !@1 . The first action of the tree is g !0 which indeed matches with g !@1 if and only if @1 gets the possible value 0 . Now, let's try to check the next action of the tree which is g !succ(0) . For it to match with g !@1 , we must have @1 = succ(0) , which implies (@1 being already equal to 0 ) that 0 = succ(0) . This is obviously false . Therefore g !@1 doesn't match with g !succ(0) (in the current context). Hence, the formula doesn't hold. This very example underlines the fact that symbolic values are global (there is only one with the same name for each formula). This can be very misleading. To prove this, let's consider the following alternate specification of the buffer process:

process buffer[in1, out]:noexit:=
	in1 !0; out !0; buffer[in1, out]
	[]
	in1 !1; out !1; buffer[in1, out]
endproc

Obviously, the two specifications are equivalent (it is a bit buffer). So, the formula that held on the previous specification should also hold on this one. That's indeed what happens but it doesn't actually check what it is supposed to. Let's take a closer look at what happens when we try to check that the formula in1 !@1 --> af(out !@1) holds on each node of the LMC tree. First we start with the left side of the choice. We want in1 !0 to match with in1 !@1 . That's not a problem for @1 = 0, so we can check the right side of the implication. The right side is also true because out !0 matches with out !@1 (@1 being still equal to 0 ). Now we keep on going and we look at the other choice. We check the matching of in1 !1 andin1 !@1 . Those two actions don't match because @1 has the value 0 . The left side of the implication is false , hence the implication is true . Therefore we can conclude that the original formula holds. However, it is clear that we didn't check that each value entering the buffer gets out. To convince oneself of this, consider the following erroneous process definition :

process buffer[in1, out]:noexit:=
	in1 !0; out !0; buffer[in1, out]
	[]
	in1 !1; out !0; buffer[in1, out]
endproc

By applying exactly the same reasoning as above, we get to the conclusion thatag(in1 !@1 --> af(out !@1)) holds. As you see, this is tricky and can easily be misleading, so one has to be very careful when using symbolic values and must keep in mind that usually a symbolic value is global to the whole formula.

However, one would like to be able to check that every value that comes in the buffer will get out. That's why we allowed the dynamic creation of symbolic values. To do so, we allow ?-experiments in the formulas. Each time the action matches another one, a new symbolic value with the given name is created. Let's notice at this point that when we do so we loose the property that a symbolic value is uniquely identified by its name. Let's see an example of a formula using this feature:

ag(in1 ?@1 --> af(out !@1))

And let's try to check this formula on the second version of the buffer. When we check the matching of in1 ?@1 with in1 !0 we create a symbolic value named@1 which immediately gets the value 0 . After this we check the right side of the implication. To do so, we must check that out !@1 (with @1 = 0 ) matches with out !0 . This is obviously true . Now we must go to the alternate path and check the matching of in1 ?@1 within1 !1 . Another symbolic value named @1 is created and gets the value 1 . After this we are left to check that out !@1 (with @1 = 1 ) matches with out !1 . It is obviously true and we can conclude that the formula holds. A by-product of this reasoning is that the proposed formula really checks what we want. This is comforted by the fact that applying the same reasoning to the erroneous buffer specification leads to the conclusion that the formula is false .

In the definition of symbolic values we mentioned a set of equations associated with each symbolic value. The model checker cannot solve the equations by itself so, it assumes they are true and gives the user the sets of equations associated to the symbolic values appearing in the formula. In our last example the model checker would actually answer that the formula holds assuming that [@1 = 0] and [@1 = 1] which are the two sets of equations (one for each symbolic value named @1 created). In this case, each set of equation is in fact made of only one equation. That's not always the case and the general form of the set is [equation1 and equation2 and ... and equationN] .

The use of symbolic values can be very convenient and lends a great power of expression to temporal logic formulas. However, they can easily mislead the user. Using them requires caution and a good understanding of the mechanisms presented here.

Syntax of the formulas

The syntax presented here is valid for the stand-alone version of LMC and will probably be slightly different in the xeludo version. Two important things to notice that are linked to the use of the prolog parser to parse formulas:

The formula must end with a . (dot) when you enter it
All the symbols starting with capital letters must be quoted. That's especially intended for all the as it appears in the spec found in this description. To give an example, if you have a gate S in your spec and you want it to appear in your formula, you must quote it. The result being for example ag('S' ! *) . This also holds for the operators leading to ADT expressions such as 'Succ'('Succ'('Succ'(0))) . So, try to avoid using capitals too often in your spec...:)

LMCExp =
( Action
| deadlock
| true
| false
| ag(LMCExp)
| eg(LMCExp)
| ax(LMCExp)
| ex(LMCExp)
| af(LMCExp)
| ef(LMCExp)
| all(UntilPlus)
| some(Until)
| LMCExp --> LMCExp
| LMCExp or LMCExp
| LMCExp & LMCExp
| ~ LMCExp
)
Until =
LMCExp until LMCExp
UntilPlus =
( Until
| LMCExp before LMCExp
| LMCExp after LMCExp
)
Action =
Gate ExperimentL GuardL
GuardL =
[Guard, Guard, ...]
Guard =
ADT
Gate =
exit /* Exits are actions on gate exit... */
name of the gate as it appears in the spec
ExperimentL =
Experiment Experiment ... Experiment 
Experiment =
! ADT
? SymVal
ADT =
op(ADT, ..., ADT) of Sort
op(ADT, ..., ADT) /* op in an operation as it appears in the
spec. */
*
SymVal of Sort
SymVal
SymVal =
@Num
Sort =
The sort as it appears in the spec.

lotos-mgr@csi.uottawa.ca