Previous Up Next

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 model-checking-style examples are provided.
Games
Bedwyr allows for a simple approach to explore for winning strategies in some simple games, such as tic-tac-toe.
λ-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, 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.

Previous Up Next