Home - AndersKaareEide/MCGAL GitHub Wiki

Welcome to the MCGAL wiki!

MCGAL is a visual model checking tool for Group Announcement Logic intended to aid fledgling logicians grasp how the various operators of the logic work.

Installation

As MCGAL is written in Kotlin, it requires Java to be installed on your computer in order to run.

Aside from this, running MCGAL should be as simple as grabbing and unzipping the latest release from https://github.com/AndersKaareEide/MCGAL/releases

The zipped archive also contains a few example models that can be interesting to look at.

Usage

When first starting the tool, you will see the screen below.

The models are visualized as circular states, with the propositions listed below each state. The lines between states indicate which states are considered indistinguishable, with the list of agents the relation is valid for written below each line.

The tool features standard load/save functionality through the menu bar at the top of the window and as previously mentioned is also bundled with a few interesting models which can be loaded from here.

On the right side of the window is where you manage the agents and propositions in your model. To change the propositions which are valid in a state or the agents that consider two states indistinguishable you can ctrl-click(cmd-click on mac) any state or line.

The bottom of the window is where you can check any formulas you write in the text field against your model. When checking a formula, the states in the model will light up to indicate which satisfy the given formula. While a formula is being checked you can also mouse over individual sub-formulas to see which states satisfy each part of the formula.

Note that in order to make formulas easier to type on a keyboard, most operators use different symbols. The full list of operators and their keyboard representation is listed below.

• Negation (¬): !
• Disjunction (v): |
• Conjunction (Λ): &
• Implication (→): -> (Dash followed by greater than)
• Knowledge (Kaφ): KA(φ) Where φ is some formula, note that the parenthesis are required
• Public announcement ([φ]ψ): [φ]ψ
• Group announcement [G]φ: [Ann,Bob]φ (Assuming G = {Ann, Bob})

Dual operators and biimplications are not currently supported directly.

The tool also features an interactive 'stepping' mode for checking formulas, where you can go through the checking process step-by-step in order to visualize how the program checks each part of the formula.

When you click 'step through' and select a state in your model, the tool will open a third tab where you manage agents and props. From here, you can skip to any step of the checking process and see the valuations of each subformula change for each step and which symbol and state the stepper is currently checking.