modality-lang 0.1.6

Modality language lib
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

// graph with a single node and a transition mapping back to itself
model InitialModel:
  graph g1:
    n1 --> n1

// graph with a acyclic set of three nodes, where +blue is on each of the transitions between them
model Model1:
  graph g1:
    n1 --> n2: +blue
    n2 --> n3: +blue

// graph with a cycle of three nodes, where +blue is on each of the transitions between them
model Model3:
  graph g1:
    n1 --> n2: +blue
    n2 --> n3: +blue
    n3 --> n1: +blue

// graph with a cycle of three nodes
model Model4:
  graph g1:
    n1 --> n2: +blue -red
    n2 --> n3: +blue -green
    n3 --> n1: -blue +red

// model with two graphs
model Model5:
  graph g1:
    n1 --> n2: +blue -red
    n2 --> n3: +blue -green
    n3 --> n1: -blue +red
  graph g2:
    n1 --> n1: +yellow

// example where current state is specified, note that state may be non-deterministic
model Model6:
  graph g1:
    n1 --> n2: +blue -red
    n2 --> n3: +blue -green
    n3 --> n1: -blue +red
  graph g2:
    n1 --> n1: +yellow
  state:
    g1: n1 n2
    g2: n1


// boolean formulas
formula FormulaTrue: true
formula FormulaFalse: false
formula FormulaBooleanWff: (true or false) and true

// true within Model1
formula FormulaDiamondBlueTrue: <+blue> true
formula FormulaBoxNegBlueFalse: [-blue] false
formula FormulaBoxNegBlueTrue: <+blue> <+blue> [-blue] false

formula FormulaBlueYellowTest1: <+blue -yellow> true // false within Model6 because yellow is not on the transition
formula FormulaBlueYellowTest2: <+blue +yellow> true // true within Model6
formula FormulaBlueYellowTest2: <+blue> true // true within Model6, absence of yellow is irrelevant