--------------------- UCTL TEMPORAL LOGIC STRUCTURE  ---------------------------

The basic temporal logic operators of UCTL/COWS are the same as the UCTL/UMC 
flavour of the logic.
In the following we present the basic syntax of them.
 
SYNTAX:

  true,    false,   statepredicate          = BASIC PREDICATES

  not form  (~ form)
  form and  form  (form & form)             = BASIC BOOL OPS
  form or  form   (form | form)
  form implies form  (form -> form)

  EF form, EG form, AF form,  EG form,      = EVENTUALLY / ALWAYS

  E[ form U form]                           
  E[ form {act} U form]                     = UNTIL KIND 1
  A[ form {act} U form]                     

  E[ form {act} U {act} form]               = UNTIL KIND 2
  A[ form {act} U {act} form]               

  <> form
  <act> form                                = DIAMOND
  <<act>> form                              = WEAK DIAMOND

  [] form
  [act] form                                = BOX
  [[act]] form                              = WEAK BOX

 max Z: form                                = max fix point
 min Z: form                                = min fix point

SEMANTICS:

the semantics of these general purpose UCTL temporal operators is described in detail 
in then UMC-Logics pdf document.

NOTES:
Max and  Min fixpoint operators are not as optimized has the other ACTL like operators 
(until, weakbox, weakdiamond) which allow a formula to be evaluated with a complexity 
which at most linear w.r.t the size of the model.
------------------------------------------------------------------------------------

Apart from these general purpose UCTL temporal operators, each customization of the
logic has its own specific (UML/COWS/..)  STATEPREDICATES  and ACTIONS.

STATEPREDICATES are the logic formulae (statepredicate) whose validity can be establish by 
observing the ground labelling of system state.

ACTIONS are the expression (act) appearing inside box, diamond, until operators used to 
specify when the gound labelling of a system transition satisfies a requested condition.

In the following we present we COWS flavour of them.

SYNTAX:

In UCTL/COWS (ground) statepredicate and actions have the form:

[executing-term ":"] [partner "."] [operation modality [args]]

  or the form:

"kill" [ "(" killname ")"]

where   modality  =  "?"  or  "!"
where   args =  "<" arg "," arg "," ... ">"
where:  executing-term, partner, operation, killname and args  = identifiers, values, "*"

examples:      termid:object.operation?<*,12>,   op?<X>  p.*!<1,nn>

SEMANTICS:

A statepredicate is TRUE in a system state if in that state there is a term
which has the syntactic immediate capability of performing a corresponding action.

E.g.   in the state modelled by the term:   "p.o!<3>|[X]q.s?<X>.nil"   (which has no evolutions)
the following ground statepredicates are true:    (p.o!), (*.*!<3>), (s?<X>), (q.s?), (q.s?<*>)

An action is TRUE for a system evolution, if the one of the term-actions executed by
the system evolution matches the action.

E.g. given the state modelled by the term  "p.o!<3>|[X]p.o?<X>.nil" 
which has a unique evolution in which two subterms synchronize on p.o, 
executiong the two term-actions  "p.o!<3>"  and "p.o?<X>", 
the following UCTL/COW actions are true:      p.o!, *.*!<3>, o?<X>, p.o?, p.o?<*>

EXAMPLE:

Given the system modelled by the following term:
  "p.o!<3> | [X]p.o?<3>.nil | p.o!<4> " 

The following formulas  are TRUE:

  (p.o!<3>)              -- statepredicate:  initial state has p.o!<3> capability
  <p.o!> true            -- It is possible an evolution step executing the action "p.o!"
  [p.o?<3>] not p.o!<3>  -- after a "p.o!<3>"  action we have no more the p.o!<3> capability
  (p.o!<4>)              -- statepredicate:  initial state has p.o!<4> capability
  <true> (p.o!<4>)       -- in one next state the system has a  p.o!<4> capability
-----------------------------------------------------------------------

Since Version 0.4  UCTL/COWS temporal operators have been extended with PARAMETRIC FORMULAS.
A parametric formula has the form:

SYNTAX:

<act($)> FORM(%)
<<act($)>> FORM(%)
[act($)] FORM(%)
[[act($)]] FORM(%)

where act($) is a parametric action containing a $ parameter,
Inside an action expresion, the $ may appear at the place of the executing-term,
at the place of a partner name, operation name or parameter.

FORM(%) is a parametric formula containining a % parameter.
Inside a formula the % parameter may appear inside the expression of
a statepredicate  or inside UCTL/COWS actions, at the place of the executing-term,
at the place of a partner name, operation name or parameter.
 
Parametric formulas cannot be nested.

Parametric actions can have a most one $variable

% pĆarameters cannot appear insidethe body of fix-point operations unless the whole
parametric formula is nested inside the fixpoint.

EXAMPLES:

[request!<$>] AF <response(%)> true


SEMANTICS:

The meaning of <act($)>FORM(%)  is
exist v such that  <act(v)>FORM(v)  is true.

The meaning of <<act($)>>FORM(%)  is
exist v such that  <<act(v)>>FORM(v)  is true.

The meaning of [act($)] FORM(%)  is
forall v [act(v)] FORM(v)  is true.

The meaning of [[act($)]] FORM(%)  is
forall v [[act(v)]] FORM(v)  is true.