
This example uses procedure `reservierung(Fahrt, Bahnhof, Bahnhof})'.

It shows how ASSL can assist in finding difficult system states. Suppose the
user is not able to add a reservation so that the new state is valid. The
generator will test every seat in the train. If it finds a valid state, the
procedure stops.

Furthermore procedure `reservierung(Fahrt, Bahnhof, Bahnhof})' is like a
typical reservation use case.

