
This directory contains two examples calling procedure
`testTrainBuildupAndWaggonOrder(Integer,Integer).

Invariant `Train::Chain' will be evaluated to false if the links
of association `WaggonOrder' form a cycle.

In the first example (run.cmd) another invariant
`Waggon::NoCycles' is loaded. The generator searches for a state,
which satisfies `Train::Chain' but not `Waggon::NoCycles'. If a
state exists, it is a counterexample showing that `Train::Chain' is
too weak. Starting run.cmd results in a `no valid state found'
message, because `Train::Chain' is correct.

The second example (run2.cmd) replaces `Train::Chain' with `Train::Chain_tooWeak',
which is too weak. Starting run2.cmd results in a counterexample showing that
`Train::Chain_tooWeak' does not prevent cycles.
