Sintaxe dos operadores temporais

A correspondência entre os operadores da lógica temporal e a correspondente notação no STeP é apresentada na tabela 2.1. Na tabela 2.2 é apresentada a correspondência para o caso dos operadores da lógica de primeira ordem.

 

Table 2.1: Operadores da lógica temporal

Operador	Significado	No STeP
$\Box p$	sempre no futuro p	[] p
$\Diamond p$	algures no futuro p	<> p
$p \mathcal{W} q$	p á espera de q	p Awaits q
$\Circle p$	no próximo instante p	() p
$\ldots p$	sempre no passado p	[-] p
$\ldots p$	algures no passado p	<-> p
$p \mathcal{B} q$	p desde quando q	p Backto q
$\circleddash p$	no instante anterior p	(-) p
$P \Rightarrow Q$	$\Box (P \supset Q)$	P ==> Q
$P \Leftrightarrow Q$	$\Box (P \supset Q) \land \Box (Q \supset P)$	P <==> Q

 

 

Table 2.2: Operadores da lógica de primeira ordem

Operador	No STeP
$\lnot p$	~p ou !p
$p \land q$	p /\ q
$p \lor q$	p \/ q
$p \supset q$	p -> q
$p \equiv q$	p <-> q
$\forall u \cdot p$	Forall u.p
$\exists u \cdot p$	Exists u.p
$\exists! u \cdot p$	Exists! u.p

 

A utilização das marcas para especificar propriedades temporais no STeP é ligeiramente diferente do método seguido nas aulas teóricas e em [5]. Segundo a notação seguida nas aulas teóricas, para cada marca m existente numa especificação em SPL, é automaticamente gerado um símbolo proposicional $at\_m$ que tem o valor verdadeiro quando a execução do programa se encontra nessa marca. No STeP em vez do símbolo $at\_m$ é usada a própria marca para especificar esse facto. Por exemplo, para especificar a propriedade de exclusão mútua no programa da figura 1.6 teríamos, na notação das aulas teóricas:

$$\Box \lnot (at\_l3 \land at\_m3)$$

A mesma propriedade seria especificada no STeP como:

[] !(l3 /\ m3)