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
{{fileException.toString()}}
Notes
Graph
Layout Graph Automatically
Automatic Zoom
{{tsException.toString()}}
Labeling Algorithm
clear
prev
next
solve
{{phi.toString()}}
{{s.id}}
{{getLabel(s, phi)}}
{{t.text}}
{{t.text}}
Repeat:
{{t.text}}
until there is no change
Formula
run algorithm
use adequate set of connectives
direct EG
{{phiException.toString()}}