PVTool

PTS Syntax

PTS expressions are a list of state declarations on the form:

ID := aps choice ;

where

ID is the identifier assinged to the state,

aps is a comma separated list of atomic propositions (e.g. ap1, ap2, ap3),

choice is a plus sign separated list of outgoing transitions of the form:
exp ID , and

exp is a linear expression that may include parameters (e.g. 5 + 2p + 3q).

Example

The PTS expression

s1 := a 5 s1 + 2p s2 ;
s2 := b q s1 ;

induces the PTS

PTL Syntax

PTL expression are generated from the two-stage syntax:

Φ , Ψ := T | F | a | Φ & Ψ | Φ | Ψ | E φ | A φ
φ := Φ U exp Ψ | X exp Φ

where

a is an atomic proposition, and

exp is a linear expression that may include parameters (e.g. 5 + 2p + 3q).