CMCV - CTL Model Checking Visualizer
Help
Transition System
--choose example--
Printer
kripke-structure-wikipedia
ss04-1-4
ss04-2-4
ss04-3-4
ss05-1-4
ss05-2-4
ss05-3-4
ss06-1-4
ss06-2-4
ss06-3-4
ws06-1-4
ws06-2-4
ws06-3-4
ws07-1-4
ws07-2-4
ws07-3-4
ws08-1-4
ws08-2-4
ws09-1-4
ws09-2-4
ws09-3-4
ws10-2-4
ws10-3-4
ws11-1-4
ws11-2-4
ws11-3-4
ws12-2-4
ws12-3-4
ws13-1-4
Load
Save
Edit
Notes
Graph
Layout Graph Automatically
Automatic Zoom
Labeling Algorithm
clear
prev
next
solve
Repeat:
until there is no change
Formula
run algorithm
use adequate set of connectives
direct EG