Syntax of Properties

Property Logic

You will find here documentation syntax of possible properties in a GAL file.

The properties currently supported are one of :

  • Safety Properties : assertions over the reachable states, regardless of how they are reached. This includes queries such as :
    • Can I reach such a state ?
    • Is this boolean assertion an invariant ?
    • What is the maximum value of this variable ?
  • CTL properties : assertions over the (infinite) computation tree, where you can observe branchings from a given state. This includes properties such as :
    • Can I reach a state that has no successors (deadlock) ?
    • Whenever this (failure) situation is reached, can we guarantee that eventually a (desired) situation will be reached ?
    • From any reachable state, does there exist a path to a state satisfying some condition ?
  • LTL properties : assertions over the set of infinite runs that the system allows. This includes properties such as :
    • Can this event occur infinitely often ?
    • Given that this event occurs infinitely often (fairness constraint), does this property hold ?

Properties are added at the bottom of a GAL file; each property is introduced by the keyword property followed by its unique name, its type, and the body of the property definition.

After writing the properties, right click the GAL file to “Run As -> ITS Model-check” to get the analysis results.

Atomic propositions

Atomic propositions reuse the expression syntax for Boolean expressions, with some additional constraints and features.

The context of the property is always the context of the main instance of the specification. If that is a GAL type, simply use the same syntax as GAL boolean expressions. If it is a composite, use a column : to access nested variables (see examples on Composite page).

Array indexes must be constants, tab[2] is ok, tab[b] is not because b is a variable.

Safety Properties

These properties can be verified by building the state space. its-reach is the primary solver for this category of problems.

This small example shows the syntax for declaring these properties.


gal System {
	int a=0;
	int b=1;
	int c=2;
	array [3] tab;
	/// more variables 
	transition a2b [b>=1] {
		a+=1;
		b-=1;
	}
	/// and transitions...
}
main System ;

property p1 [reachable] : a==1 && b==0;
property p2 [invariant] : a==0 && tab[1]==0;
property p3 [never] : a==1 ;

property b1 [bounds] : a;
property b2 [bounds] : a + b + tab[0] + c;

Reachable, Invariant, Never

For these three types of properties, a Boolean expression is expected as body for the property.

  • reachable : true if at least one reachable state satisfies the predicate
  • invariant : true if all of reachable states satisfy the predicate
  • never : true if none of the reachable states satisfy the predicate

Never and invariant are dual of one another, which one you use is a matter of preference. Never is typically used to specify undesired behavior, whereas invariant is used for desired ones, so that “true” formulas means the system is doing what it should.

Bounds

Bounds are a useful tool to understand variable domains better. The body of a bounds property is either a single variable, or a sum of variables. The tool will answer with the minimal and maximum value of the provided sum of variables.

e.g.

Bounds property b1 :0 <= a <= 1
Bounds property b2 :0 <= a+b <= 1

Note that for b2 the tool does not actually report what was asked for a + b + tab[0] + c ; this is due to variable simplifications. In this example all cells in the array tab are always 0 and c is always 2.

The tool does warn that it is simplifying variables away :

INFO:Removed 1 constant variables :c=2
INFO:Removed constant array :tab[]

And will print a message :

WARNING:For property b2 will report bounds of ((a+b)+2) without constants. Add 2 to the result in the trace.

CTL

CTL properties are built from the following operators where p and q are CTL formulas.

  • true, false, comparison of a variable to a constant : atomic predicates. The syntax of boolean predicates is currently (June 2017) still very limited in CTL.
  • Usual Boolean connectors : AND &&, OR ||, NOT !
  • Unusual Boolean connectors (but very useful for CTL) : IMPLY ->, EQUIVALENCE <->
  • Temporal operators :
    • EF(p), EX(p), E(p U q), EG(p) : existential modalities for Finally, neXt, Until, and Generally.
    • AF(p), AX(p), A(p U q), AG(p) : universal modalities

Parenthesizing is necessary, the parser likes it that way, so add parenthesis until it’s happy (no more red underline).

The semantics are not quite text-book; in presence of deadlocks, EG p will stutter and accept dead states satisfying p. This does not affect the semantics of EX, AX, so that AG (EX (true)) does test for absence of deadlocks. For a more formal presentation of this semantics see this document Aalborg University, TAPAAL team’s CTL semantics document, used in the MCC. These semantics are more natural for reasoning.

For instance, AF(p) when some deadlock states satisfying !p are reachable without ever validating p, but there are no loops or SCC satisfying !p:

  • is true with textbook semantics, because it reduces to ! (EG !p), so that a reachable deadlock state satisfying !p is not accepted as a counter example
  • is false with the semantics we use, a path satisfying !p to a deadlock state satisfying !p is indeed a counter-example

This small example shows some CTL properties on a simple three philosopher example.



gal Philo {
	int think = 1 ;
	int waitL = 0 ;
	int waitR = 0 ;
	int hasL = 0 ;
	int hasR = 0 ;
	int eat = 0;
	int fork = 1 ;

	transition ask [think >= 1] {
		think-= 1 ;
		waitR+= 1 ;
		waitL+= 1 ;
	}
	transition getL [waitL >= 1 && fork >=1] {		
		fork-= 1 ;
		waitL-= 1 ;
		hasL+= 1 ;
	}
	transition giveFork [fork >= 1] label "takeFork" {
		fork-=1;
	}
	transition returnFork [true] label "returnFork" {
		fork+=1;
	}	
	transition getR [waitR >= 1] label "getRight" {
		waitR -= 1 ;
		hasR += 1 ;
	}
	transition eat [hasR >= 1 && hasL >= 1] {
		eat += 1 ;
		hasL-=1 ;
		hasR-=1 ;
	}	
	transition release [eat >= 1] label "endEat" {
		eat-=1;
		fork+=1;
		think+=1;
	}
}

composite ThreePhilo {
	Philo p0;
	Philo p1;
	Philo p2;
		
	synchronization get0 {
		p0."getRight";
		p1."takeFork"; 
	}
	synchronization end0 {
		p0."endEat";
		p1."returnFork"; 
	}
	synchronization get1 {
		p1."getRight";
		p2."takeFork"; 
	}
	synchronization end1 {
		p1."endEat";
		p2."returnFork"; 
	}
	synchronization get2 {
		p2."getRight";
		p0."takeFork"; 
	}
	synchronization end2 {
		p2."endEat";
		p0."returnFork"; 
	}
}

main ThreePhilo ;

// Test for absence of deadlocks
property noDeadlocks [ctl] : AG(EX(true)) ;

// p0 and p2 never eat simultaneously.
property mutEx [ctl] : AG (! (p0:eat==1 && p2:eat==1));

// Whenever philosopher 0 finishes eating, philosopher 1 **can** eat before philo 0 eats again.
property turns [ctl] : 
	AG (p0:eat==1 
		-> (
			A p0:eat==1 U 
				p0:eat==0 && 
				(E p0:eat==0 U p1:eat==1) 
			)		
	);


// Whenever philosopher 0 finishes eating, he cannot eat again until philosopher 1 has eaten.
property fair [ctl] : 
	AG (p0:eat==1 
		-> (
			A p0:eat==1 U 
				p0:eat==0 && 
				(A p0:eat==0 U p1:eat==1) 
			)		
	);

// Philo 0 will be the first to eat
property firstEater [ctl] : 
	A  (p1:eat==0 && p2:eat==0) U  p0:eat==1 ; 

// Existence of a home state (a.k.a reset property)
property home [ctl] :
	AG ( EF (p0:eat==0 && p1:eat==0 && p2:eat==0 ));

LTL

LTL properties are built from the following operators where p and q are LTL formulas.

  • true, false, comparison of a variable to a constant : atomic predicates. The syntax of boolean predicates is decently permissive as long as all variables in the expression belong to a single GAL instance, but comparisons of variables belonging to different subcomponents is not supported.
  • Usual Boolean connectors : AND &&, OR ||, NOT !
  • Unusual Boolean connectors (but very useful for LTL) : IMPLY ->, EQUIVALENCE <->
  • Temporal operators :
    • p U q, , p W q, p M q, p R q : operators for Until, Weak Until, Strong Release, and Release
    • F p, G p, X p : Future, Generally and neXt operators

The parser is relatively lenient, but parenthesizing still avoids surprises. For more info on LTL operators and their semantics, please visit Spot or play with their excellent online LTL to Buchi tool.

Tags: