#2 Rodin project example for getting started.

[Anonymous]

Is it possible to make a small Rodin project
available , in order to easily get started? I am
getting frustrated by syntax errors which I cannot
understand e.g., how should a simple if should be
written?

IF counter = 2 THEN counter :=0 ELSE counter :=
counter + 1 END

as an action gives a syntax error: 'invalid
assignement'.

Though this seems inline with B syntax...

Regards,
Renaud

[Farhad Mehta]

Logged In: YES
user_id=1026923

This does not seem to be in line with the new Event-B
syntax. What you want is to create a new machine with:

Variables:
counter

Invariants:
counter : NAT

Events:

evt1:
grd1: counter = 2
act1: counter := 0

evt2:
grd1: counter /= 2
act1: counter := counter + 1

We will put up an example project as soon as the file
structures are a bit more stable.

Cheers,
Farhad