PVTool

### PTS Syntax

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

$\mathrm{ID}:=\left\{\mathrm{aps}\right\}\mathrm{choice};$

where

$\mathrm{ID}$ is the identifier assinged to the state,

$\mathrm{aps}$ is a comma separated list of atomic propositions (e.g. ap1, ap2, ap3),

$\mathrm{choice}$ is a plus sign separated list of outgoing transitions of the form:
, and

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

#### Example

The PTS expression

induces the PTS

### PTL Syntax

PTL expression are generated from the two-stage syntax:

$\Phi ,\Psi \phantom{\rule{0.1em}{0ex}}:=\phantom{\rule{0.8em}{0ex}}T\phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}F\phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}a\phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}\left[\Phi \right]&\left[\Psi \right]\phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}\left[\Phi \right]|\left[\Psi \right]\phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}E\phi \phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}A\phi$
$\phantom{\rule{1.4em}{0ex}}\phi \phantom{\rule{0.3em}{0ex}}:=\phantom{\rule{0.8em}{0ex}}\left[\Phi \right]U\left\{\mathrm{exp}\right\}\left[\Psi \right]\phantom{\rule{1em}{0ex}}|\phantom{\rule{1em}{0ex}}X\left\{\mathrm{exp}\right\}\left[\Phi \right]$

where

$a$ is an atomic proposition, and

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