[Top]
 

MBP: SMV language interface


Index


Standard SMV language

SMV is the input language to the NuSMV model checker. It allows describing a system as a Finite State Machine, to declare invariants and temporal requirements that must be obeyed by it. On-line documentation can be found here.

MBP custom SMV language

MBP applies the following variants to the SMV language:


A domain/problem example

This is an SMV encoding of the saturation/balancing domain and problem presented here: three engines can be driven to increase/decrease their power; the requirement is that the maximum power level has to be reached, maintaining engines "balanced", that the maximum delta between the engines' powers must be 1.

This encoding is action-centered: every ground action is translated as a TRANS conjunct. Action preconditions are DEFINEd and enforced by requiring their effect to be FALSE.

MODULE main
DOMAINNAME saturation_balancing
PROBLEMNAME satbal_pb
PROBLEMDOMAIN saturation_balancing
IVAR
action: {inc1,inc2,inc3,dec1,dec2,dec3,nop};

VAR
desired:0..6;
pow1:0..2;
pow2:0..2;
pow3:0..2;

INIT
(pow1=0) & (pow2=0) & (pow3=0) & desired=0

DEFINE
prec_inc1:=(!(pow1 = 2));
prec_inc2:=(!(pow2 = 2));
prec_inc3:=(!(pow3 = 2));
prec_dec1:=(!(pow1 = 0));
prec_dec2:=(!(pow2 = 0));
prec_dec3:=(!(pow3 = 0));
prec_nop:=TRUE;
TRANS
( ((action=inc1 & prec_inc1) -> ((next(pow1)=(pow1 + 1) & next(desired)=desired & next(pow2)=pow2 & next(pow3)=pow3)))
&
(action=inc1 & !prec_inc1 -> FALSE) )
TRANS
( ((action=inc2 & prec_inc2) -> ((next(pow2)=(pow2 + 1) & next(desired)=desired & next(pow1)=pow1 & next(pow3)=pow3)))
&
(action=inc2 & !prec_inc2 -> FALSE) )
TRANS
( ((action=inc3 & prec_inc3) -> ((next(pow3)=(pow3 + 1) & next(desired)=desired & next(pow1)=pow1 & next(pow2)=pow2)))
&
(action=inc3 & !prec_inc3 -> FALSE) )
TRANS
( ((action=dec1 & prec_dec1) -> ((next(pow1)=(pow1 - 1) & next(desired)=desired & next(pow2)=pow2 & next(pow3)=pow3)))
&
(action=dec1 & !prec_dec1 -> FALSE) )
TRANS
( ((action=dec2 & prec_dec2) -> ((next(pow2)=(pow2 - 1) & next(desired)=desired & next(pow1)=pow1 & next(pow3)=pow3)))
&
(action=dec2 & !prec_dec2 -> FALSE) )
TRANS
( ((action=dec3 & prec_dec3) -> ((next(pow3)=(pow3 - 1) & next(desired)=desired & next(pow1)=pow1 & next(pow2)=pow2)))
&
(action=dec3 & !prec_dec3 -> FALSE) )
TRANS
( ((action=nop & prec_nop) -> ((next(desired)=desired & next(pow1)=pow1 & next(pow2)=pow2 & next(pow3)=pow3)))
&
(action=nop & !prec_nop -> FALSE) )

FULL_OBS_CTL_GOAL
AF (6 = (pow1 + pow2 + pow3)) &
AG (!(pow1 > (pow1 + 1))) &
AG (!(pow1 > (pow2 + 1))) &
AG (!(pow1 > (pow3 + 1))) &
AG (!(pow2 > (pow1 + 1))) &
AG (!(pow2 > (pow2 + 1))) &
AG (!(pow2 > (pow3 + 1))) &
AG (!(pow3 > (pow1 + 1))) &
AG (!(pow3 > (pow2 + 1))) &
AG (!(pow3 > (pow3 + 1)))

Other encoding styles are possible, e.g. describing the evolution of each variable using the ASSIGN and CASE constructs. For this example, this leads to a more compact representation (and to faster plan construction):

MODULE main
DOMAINNAME saturation_balancing
PROBLEMNAME satbal_pb
PROBLEMDOMAIN saturation_balancing
IVAR
action: {inc1,inc2,inc3,dec1,dec2,dec3,nop};

VAR
desired:0..6;
pow1:0..2;
pow2:0..2;
pow3:0..2;

INIT
(pow1=0) & (pow2=0) & (pow3=0) & desired=0

DEFINE
prec_inc1:=(!(pow1 = 2));
prec_inc2:=(!(pow2 = 2));
prec_inc3:=(!(pow3 = 2));
prec_dec1:=(!(pow1 = 0));
prec_dec2:=(!(pow2 = 0));
prec_dec3:=(!(pow3 = 0));
prec_nop:=TRUE;

ASSIGN next(pow1) :=
case
(action = inc1) & prec_inc1 : pow1 + 1;
(action = dec1) & prec_dec1 : pow1 - 1;
1 : pow1;
esac;

ASSIGN next(pow2) :=
case
(action = inc2) & prec_inc2 : pow2 + 1;
(action = dec2) & prec_dec2 : pow2 - 1;
1 : pow2;
esac;

ASSIGN next(pow3) :=
case
(action = inc3) & prec_inc3 : pow3 + 1;
(action = dec3) & prec_dec3 : pow3 - 1;
1 : pow3;
esac;

FULL_OBS_CTL_GOAL
AF (6 = (pow1 + pow2 + pow3)) &
AG (!(pow1 > (pow1 + 1))) &
AG (!(pow1 > (pow2 + 1))) &
AG (!(pow1 > (pow3 + 1))) &
AG (!(pow2 > (pow1 + 1))) &
AG (!(pow2 > (pow2 + 1))) &
AG (!(pow2 > (pow3 + 1))) &
AG (!(pow3 > (pow1 + 1))) &
AG (!(pow3 > (pow2 + 1))) &
AG (!(pow3 > (pow3 + 1)))
 


A plan example

The following plan solves the problem above by cyclically increasing, in turn, the power of each engine.

PLAN smartplan
PLANNAME smartplan
PLANPROBLEM satbal_pb
PLANDOMAIN satbal
PLANVAR
pc:{system_9,system_8,system_0,system_3};
INIT
pc=system_0
EVOLVE
case
(pc = system_0):
case
(!(6 = pow1 + pow2 + pow3)):
next(pc)=system_8 & (action=inc1);
1:
next(pc)=system_3 & (action=nop);
esac;
(pc = system_8):
next(pc)=system_9 & (action=inc2);
(pc = system_9):
next(pc)=system_0 & (action=inc3);
(pc = system_3):
next(pc)=system_3 & (action=nop);
esac

Invoking MBP

For the SMV interface either plan synthesis, plan validation and plan simulation are performed by directly calling MBP.


Last edited: 2002-12-10