System invariants in GAL

[bohlender]

Hi,

I'm currently investigating the feasibility of using the GAL formalism in a side project of mine.

The current approach characterises a system's semantics in terms of the SMV formalism. This works pretty well but introduces unnecessary intermediate states that I can get rid of when using GAL instead -- in particular its fixpoint actions.

However, one feature of SMV that I cannot reproduce without jumping through hoops is the restriction of a system's state space by a given predicate -- called INVAR constraint in SMV.

My use case is that I want to check reachability of bad states B(X). However, I also have a static analysis that can quickly under-approximate the states from which B(X) cannot be reached. Therefore I would like to use this outcome (its negation) to constrain the search space, and avoid exploration of some parts that are known to never reach B(X).

I'm aware that I could do this manually with libITS, by restricting the state space after every action, but was wondering whether there is already an easy way to restrict the state space in GAL.

[yanntm]

hi,
so you do need to do it "manually", the easiest approach is probably to create a labeled transition "invar" with an if (!B(X)) abort; then call it with self."invar" after any transition that could possibly modify (falsify is better) your B predicate. However, adding it everywhere will make the variable(s) in B part of the support of all transitions, which is not great for the symbolic engine.
I have an SMT engine https://github.com/lip6/ITSTools/blob/master/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/bmc/NecessaryEnablingsolver.java#L194-L200 I can use as oracle to determine if a transition could potentially enable/disable a given condition ; but there is no way to invoke that other than programmatically currently. An approach could be to build a tool that takes say a "invariant" type property and a system, and rewrites the system to ensure the invariant is preserved.

That is pretty doable, a few hours of dev, but sorry the feature currently does not exist. In any case the result would be the same as the manual approach, it would just be much more comfortable as you can edit both system and predicate B and don't worry about support of transitions etc...

[bohlender]

Thanks for the quick reply!

so you do need to do it "manually", the easiest approach is probably to create a labeled transition "invar" with an if (!B(X)) abort; then call it with self."invar" after any transition that could possibly modify (falsify is better) your B predicate. However, adding it everywhere will make the variable(s) in B part of the support of all transitions, which is not great for the symbolic engine.

This is exactly the workaround I'm using right now.

I have an SMT engine https://github.com/lip6/ITSTools/blob/master/smt/fr.lip6.move.gal.gal2smt/src/fr/lip6/move/gal/gal2smt/bmc/NecessaryEnablingsolver.java#L194-L200 I can use as oracle to determine if a transition could potentially enable/disable a given condition ; but there is no way to invoke that other than programmatically currently.

Doing the restriction programmatically is what I actually what I meant by doing it "manually". I was just wondering whether I'm missing a more convenient way of accomplishing the restriction in GAL.

An approach could be to build a tool that takes say a "invariant" type property and a system, and rewrites the system to ensure the invariant is preserved.

That is pretty doable, a few hours of dev, but sorry the feature currently does not exist. In any case the result would be the same as the manual approach, it would just be much more comfortable as you can edit both system and predicate B and don't worry about support of transitions etc...

I would like this. However, depending on whether you find this useful to have in GAL/ITSTools, feel free to close this issue or keep it open as an enhancement/feature request.

[yanntm]

What would that look like syntactically, I'm not sure.
Perhaps

// gal and composite definitions
main Toto / [invariant] a<=3 && ... ;

So the system is built / under assumption of, and then we reuse the property invariant syntax, to define a predicate.

From that the transitions are enriched, where appropriate, with a post-test of the condition. Naive approach just adds to all transitions.

Do you have an example of SMV style declaration of system with invariant constraint ?

[bohlender]

// gal and composite definitions
main Toto / [invariant] a<=3 && ... ;

So the system is built / under assumption of, and then we reuse the property invariant syntax, to define a predicate.

Yes, it it is pretty much the same syntax in SMV, except that there the invariant is written inside the component it constrains.

Do you have an example of SMV style declaration of system with invariant constraint ?

I've attached a single-module example that characterises a single-agent search problem instance (aka. the box-pushing puzzle Sokoban). The following excerpt illustrates where the restricting predicate, following the INVAR keyword, is introduced. The actual invariant that is to be checked is specified after INVARSPEC, at the bottom.

MODULE main
	IVAR
		dir : {UP, DOWN, LEFT, RIGHT};
	VAR
		px : 0..14;
		py : 0..4;
		boxes : array 0..4 of array 0..14 of boolean;
	INVAR
		... & !boxes[2][1] & !boxes[2][13] & ...
	DEFINE
		...
	ASSIGN
		init(px) := 12; init(py) := 2;
		...
		next(px) := case
			dir=LEFT  & (leftStep | leftPush)   : px - 1;
			dir=RIGHT & (rightStep | rightPush) : px + 1;
			TRUE : px;
		esac;
		...
INVARSPEC
	!(boxes[3][2] & boxes[3][3] & boxes[3][4] & boxes[3][5] & boxes[3][6])

This simple example takes nuXmv's BDD-based engine 17s without the INVAR, but just 4s with INVAR added.

[yanntm]

ok, interesting use case.

I need some more time to think about how it could be done. Defining invariants at component level is nicer I guess than only for main. But could different instances of a given module be specified to assume different invariants, or can we consider that all instances of a given type satisfy the type's invariants ?

I guess with an optional "invariant" constraint declared in GAL or composite types, and assuming all instances have the same (local) constraint, there is a rewriting to a GAL that exhibits the desired semantics using current syntax/semantic bricks, so this feature can be seen as pure syntactic sugar.

That is desirable, it's much easier to integrate the feature if it can be degeneralized to fall back to the "normal" case.

[bohlender]

But could different instances of a given module be specified to assume different invariants, or can we consider that all instances of a given type satisfy the type's invariants ?

A module's INVAR predicate constrains all instances of that module. However, a module may contain several instances of other modules, which could be constrained differently by the parent module's INVAR. The following artificial example illustrates the use of INVAR in both ways:

MODULE rng
    VAR
        out : unsigned word[8];
    INVAR
        out <= 0ud8_100;

MODULE main
    VAR
        c1  : rng;
        c2  : rng;
        sum : unsigned word[8];
    INVAR
        c1.out < c2.out;
    INIT
        sum = 0ud8_0;
    ASSIGN
        next(sum) := c1.out + c2.out;

INVARSPEC
    sum < 0ud8_200;

Here, the rng module is a 8-bit random number generator that is constrained to only output values in the interval [0,100]. Every instance of that module will have that restriction.

The main module features two instances, c1 and c2, of the rng module and just outputs their sum. However, the INVAR in the main module can be used restrict the instances in different ways. Being an artificial example, constraining the state-spaces of both instances to those that satisfy c1.out < c2.out is meaningless, but illustrates that the a constraint may even put different instances in relation. In particular, c1.out will never become 100 and sum never reach 200.

assuming all instances have the same (local) constraint, there is a rewriting to a GAL that exhibits the desired semantics using current syntax/semantic bricks, so this feature can be seen as pure syntactic sugar.

For my use case, having all instances constrained in the same way would be sufficient.

[yanntm]

ok, yes we could probably add that feature.

So I add one optional "invariant" declaration per gal/composite declaration, basically we enforce it as a condition on the initial state (raise an error if initial does not satisfy it) and as a post condition on every transition.

Basic strat is to add the constraint after all transitions, but this can be obviously refined,
a) using the support of transitions
b) more refined using SMT solver to decide if "could disable"

Would that match your need ?

[bohlender]

Thanks, yes, this would suffice for my use case.

[yanntm]

Just to say I still have this in the pipe, but I've been pretty busy. Did you manage to go around it manually (by adding the tests yourself) and did the result match what you wanted ? I'm still ok to implement it if you are actually using the tool and you are still interested.

[bohlender]

To be honest, I did hardly get around to work on that side project recently -- busy with writing up my PhD thesis. While I would love to have the feature added to ITSTools/GAL and will keep using it, it is not a pressing issue for me but a nice-to-have, as I also use other backends and haven't determined the best procedure yet. Feel free to keep the issue open until you find some time.

However I still think that, idependent from my side project, this feature will come in handy for many users of symbolic model checkers. When expressing systems in formalisms like GAL, it is common to have some higher-level information available, e.g. from static analyses, that one wants to incorporate, or pass down, to the model checking procedure. For example, folks at the Institute of Industrial Automation and Software Engineering (University of Stuttgart) use ITSTools to verify logic control software, and could certainly profit from integrating static analysis results.