[Top]

MBP: SMV language interface

Index

Standard SMV language
MBP custom SMV language
A domain/problem example
A plan example
Invoking MBP

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:

Domain/problem/plan names: keywords are added to indicate them (see the headers of the domain/problem example and of the plan example).
Output variables: an output variable is declared by the keyword OVAR, and its semantics is defined by OUTPUT:
- OVAR var_decl requires an SMV boolean variable declaration.
- OUTPUT simple_expr require the expression to be of the form:
  ( ( (ovar = 1) -> simple_expr) & ((ovar = 0) -> simple_expr) ) )
  where ovar is an output variable.
Goal keywords: these correspond to the goal classes handled by MBP:
- FULL_OBS_WEAK_GOAL simple_expr : weak planning under full observability.
- FULL_OBS_STRONG_GOAL simple_expr : strong planning under full observability.
- FULL_OBS_STRONG_CYCLIC_GOAL simple_expr : strong cyclic planning under full observability.
- FULL_OBS_CTL_GOAL ctl_expr : CTL planning under full observability (notice that CTL expressions are expected).
- NULL_OBS_STRONG_GOAL simple_expr : conformant planning.
- PARTIAL_OBS_STRONG_GOAL simple_expr : strong planning for full observability
Plan language: This allows defining a plan as a finite-state machine. The evolution of a plan's internal state and of its outputs are described by a specific syntax, which is esemplified in the plan example.
Unsupported/restricted SMV features: invariants and fairness constraints (INVAR, JUSTICE and COMPASSION resp.) are accepted as part of SMV syntax, but are not handled by MBP. The structure of a domain must only contain the main module (SMV processes are not handled).

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):

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.

Plan synthesis: MBP domain_problem.smv.
Where domain_problem.smv is the SMV modeling of the domain and problem (e.g. the domain/problem example).
Output of produced plan: by default, no output is produced. The -print_plan option must be used if the plan has to be given in output. In this case, the plan is given to stdout, unless a file is specified by the -output_plan_name option.
Validation of the produced plan: the produced plan is validated by adding -validate_plan. Ad-hoc efficient validation for strong plans for partially/not observable domains are performed by -po_validate_hoc and -conformant_ad_hoc_validate.
Several encoding options (e.g. -mono) and problem-specific options are available, see MBP -help.
Plan validation: MBP -skip_synthesis -validate_plan domain_problem_plan.smv
Where domain_problem_plan.smv is a file containing the SMV modeling of the domain, problem and plan (e.g. the concatenation of the domain/problem example and the plan example).
Domain simulation: MBP -skip_synthesis -dsimulate domain_problem_plan.smv
Plan simulation: MBP -skip_synthesis -simulate_plan domain_problem_plan.smv
Where domain_problem_plan.smv is a file containing the SMV modeling of the domain, problem and plan (e.g. the concatenation of the domain/problem example and the plan example).
Several simulation options are available, to allow various modalities in the simulation; see MBP -help.

Last edited: 2002-12-10