The PTTF input language syntax

The input language of the pttf tool consists of sentences encoding the
initial condition formula and a sequence of transition formulas, which
must be separated by white-space, i.e.  blanks,  tabs or newlines. The
input stream of sentences  encoding the initial condition  formula and
a set of   transition   formulas   represents   a  transition  program.

Propositional variables are   denoted  by  identifiers  consisting  of
letters, digits and the underscore character. They should start with a
letter. The letter case is significant.  Identifiers that are reserved
words cannot be used to name variables! The 1-letter operator symbol U
(until) must also not be used as variable name. 

The list   of logical  and  temporal  operators which  can  be used in
transition programs is presented below: 

Operators:              Name:

        ~               not
        /\              and
        \/              or
        ->              implies
        []              always
        @               next
        U               until

Reserved word:          Name:

        Pr              Process

The Pr reserved word is introduced to represent the disjunction of all
the propositional variables of a transition program. 

The and (/\)  operator can be omitted  when used between two transition
formulas  or between  the initial  condition   formula and a transition
formula. 

C-style comments may appear anywhere white-space is allowed. 

White-space, i.e.  blanks, tabs and newlines may  appear in any number
between any two consecutive language tokens, and  at the start and end
of the input file. 

A transition program must terminate by a point (.). 

The input language has the following syntax:

PTTF_input :

-->[ Initial_condition ]-->[ Transition_formulas ]-->(.)


Initial_condition :

-->[ Consequent ]-->


Transition_formulas :

--,-->[ Transition_formula ]--.-->
  |                           |
  `-------[ Separator ]<------'



Transition_formula :

--.----->[ ALWAYS ]-(()->[ Implication ]-())-----,->
  |                                              |
  `--(()-[ ALWAYS ]-(()->[ Implication ]-())-())-'


Implication :
 
-->[ Antecedent ]-->[ IMPLIES ]-->[NEXT]-.-(()->[ Consequent ]-())-,->
                                         |                         |
                                         `------[ IDENTIFIER ]-----'

Antecedent : 
     
---->[ Factor ]---->


Consequent : 

-->[ NOT ]-->[ PROCESS ]-->[ UNTIL ]-->[ Factor ]-->


Factor :

--.------->[ Term ]--------,->
  |                        |
  `---(()->[ Term ]-())----'
               

Term :

--,->[ Identifier ]-.->
  |                 |
  `------[ OR ]<----'


Separator :

-.--->( BLANK )--,->
 |               |
 `---->( TAB )---'
 |               |
 `->( NEW_LINE )-'

Back to pttf page