4 Released examples
Few things are harder to put up with
than the annoyance of a good example.
– Mark Twain
The distribution of Bedwyr comes with several examples of its use.
These examples can be classified roughly as follows.
- These examples are small and illustrate some
simple aspects of the system.
- Model checking
- Some simple model-checking-style examples are
- Bedwyr allows for a simple approach to explore for
winning strategies in some simple games, such as tic-tac-toe.
- Various relations and properties of the
λ-calculus are developed in some definition files.
- Simulation and bisimulation
- These relationships between
processes where an important class of examples for which the theory
behind Bedwyr was targeted. Examples of checking simulation is done
for abstract transition systems, value-passing CCS, and the
π-calculus. The π-calculus examples are of particular note:
all side-conditions for defining the operational semantics and
bisimulation are handled directly and declaratively by the logic
underlying Bedwyr. See 6 below for some more
details about the π-calculus in Bedwyr.