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.

Basic examples
 These examples are small and illustrate some
simple aspects of the system.
 Model checking
 Some simple modelcheckingstyle examples are
provided.
 Games
 Bedwyr allows for a simple approach to explore for
winning strategies in some simple games, such as tictactoe.
 λcalculus
 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, valuepassing CCS, and the
πcalculus. The πcalculus examples are of particular note:
all sideconditions 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.