This is a Spacemacs layer for mCRL2 which provides syntax highlighting, and a reasonable integration of the mCRL2 toolset via Spacemacs bindings.
| Key | Function |
|---|---|
| SPC b l 1 | Create a Linear Process Spec. based off of current buffer using Reg. |
| SPC b l 2 | Create a Linear Process Spec. based off of current buffer using Reg2. |
| SPC b l 3 | Create a Linear Process Spec. based off of current buffer using Stack. |
| SPC b t | Create a Labled Transition System. |
| SPC b b | Create a Parameterized Boolean Equation System using a previously created LTS and a modal formula found at project location "properties/testProp.mcf". |
| SPC c | Model Check using PBESolve on your created PBES and LTS. |
| SPC s | Open LPSXSim trace simulator using previously created LPS. |
| SPC g | Open LTSGraph with previously created LTS. |
| SPC e | Open LTSGraph with evidence created from Model Checking via PBESolve. |
Clone this layer into your '~/.emacs.d/private'. Then simply add 'mCRL2' as one of your configuration layers in your spacemacs config.