Skip to content
Snippets Groups Projects
Select Git revision
  • 9bdb9b6e15c2d3961b20ffc4e230eaf7b328d446
  • master default protected
2 results

Readme.md

Blame
  • user avatar
    Michael Leuschel authored
    9bdb9b6e
    History
    Code owners
    Assign users and groups as approvers for specific file changes. Learn more.

    Einstein's Puzzle for VisB

    ProB2-UI and VisB

    You will need to download a recent version of ProB2-UI for the examples below (1.1.1-SNAPSHOT or newer). It will contain the VisB view to allow visualizing states using SVG graphics and simple JSON annotations.

    Alloy Encoding of the Einstein Puzzle

    The Alloy model of the puzzle is a corrected version adapted from Stackoverflow.

    To solve it in ProB2-UI

    • select the "Symbolic" pane of the "Animation" view (bottom-left of the main window)
    • select "Sequence" and type "run0" and click on "Add and Check" (run0 is a B operation which is a translation of an Alloy command to solve the puzzle)
    • to see the visualisation Choose "Open VisB" in the visualisation menu, click on the "Open" icon in the top-right of the VisB menu bar and select the file "einstein_puzzle_als.json".

    You should then see something like the following picture:

    ProB2-UI Alloy Version of Einstein's Puzzle

    Note: you can re-create the standalone HTML export in the repo by calling the command-line version of ProB:

    probcli einsteins_puzzle.als -cbc-sequence run0 -visb_with_vars einstein_puzzle_als.json out.html

    Note that the initial solution from Stackoverflow was missing constraints, which was apparent in the visualisation (dog appeared twice).

    TLA+ Encoding of the Einstein Puzzle

    The TLA+ model is taken from the TlaPlus Examples Repo (the model initially came from DeFrain).

    To solve it in ProB2-UI

    • select the "Symbolic" pane of the "Verifications" view (middle-right)
    • choose "Invariant" and click on "Add and Check". Note: the invariant contains the negated solutions predicate: finding a counter example corresponds to solving the puzzle.
    • to see a visualisation of the solution (i.e., counter example): choose "Open VisB" in the visualisation menu, click on the "Open" icon in the top-right of the VisB menu bar and select the file "Einstein_tla.json"

    You should then see something like the following picture:

    ProB2-UI TLA Version of Einstein's Puzzle

    Note: you can re-create the standalone HTML export in the repo by calling the command-line version of ProB

    probcli Einstein.tla -cbc all -visb_with_vars Einstein_tla.json out.html