search

nl-utwente-groove / code

GROOVE code base
https://groove.cs.utwente.nl
5 stars 0 forks source link

Uniform syntax for CTL and LTL #600

Closed rensink closed 6 months ago

rensink commented 15 years ago

At the moment, the syntax for CTL and LTL formulae is too different. It would be much more user friendly to make them more alike.

Reported by: kastenberg

rensink commented 14 years ago

Original comment by: rensink

rensink commented 14 years ago

CTL syntax should be as follows:

!phi phi | psi phi & psi phi -> psi phi <- psi phi <-> psi EG(phi) AG(phi) EF(phi) AF(phi) EX(phi) AX(phi)

LTL syntax should be comform modulo path quantifiers.

Original comment by: kastenberg

rensink commented 14 years ago

"Should be", does that mean it's implemented or you're going to implement it that way?

The proposal looks good, but I'm missing the Until operators:

E(phi U phi) A(phi U phi)

resp

phi U phi

for CTL and LTL.

Moreover, we need to think about the allowed syntax for propositions! What characters may occur in a proposition? Parentheses, special chars, spaces? In any case, I think we should use single quotes to indicate an arbitrarily formatted proposition.

Original comment by: rensink

rensink commented 13 years ago

Original comment by: rensink

rensink commented 13 years ago

Original comment by: rensink

rensink commented 11 years ago

Original comment by: rensink