BSML Model Checker
Universe (Worlds)
World 1
World 2
Propositions
P1
Truth Values
World
P1
World 1
World 2
Relations
State
World 1
World 2
Formula Evaluation
M
,
s
⊨
φ
M, s \ ⊨\ \varphi
M
,
s
⊨
φ
M
,
s
⫤
φ
M, s \ ⫤\ \varphi
M
,
s
⫤
φ
Pragmatic Enrichment
M
,
s
⊨
M, s ⊨
M
,
s
⊨
Evaluate
Model Visualization
Generate Visualization