-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy path6.patch
More file actions
152 lines (139 loc) · 10 KB
/
Copy path6.patch
File metadata and controls
152 lines (139 loc) · 10 KB
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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
--- MightyPPL_new_original.cpp 2025-11-16 21:36:51.513042869 +0000
+++ MightyPPL_new_6.cpp 2025-11-11 18:12:06.068569486 +0000
@@ -1052,6 +1052,7 @@
out_str << "event:a" << std::endl << std::endl << std::endl;
out_str << "clock:1:g" << std::endl;
+ out_str << "clock:1:x" << std::endl; // for pinwheel
for (auto it = temporal_atoms.begin(); it != temporal_atoms.end(); ++it) {
@@ -1730,20 +1731,58 @@
name = "M";
clocks.insert({0, "x0"}); // clock 0 is needed anyway
+ clocks.insert({1, "x"}); // for pinwheel
locations.push_back(monitaal::location_t(true, 0, "s0", empty_invariant));
- // 0 -> 0, true
+ label = bdd_ithvar(nnf_formula->props.at("p1")) & !bdd_ithvar(nnf_formula->props.at("p2")) & !bdd_ithvar(nnf_formula->props.at("p3")) & !bdd_ithvar(nnf_formula->props.at("p4")) & !bdd_ithvar(nnf_formula->props.at("p5")) & !bdd_ithvar(nnf_formula->props.at("p6"));
+ reset.push_back(1);
+ guard.push_back(monitaal::constraint_t::lower_non_strict(1, 1));
+ bdd_edges.push_back(monitaal::bdd_edge_t(0, 0, guard, reset, label));
+ guard.clear();
+ reset.clear();
+
+ label = !bdd_ithvar(nnf_formula->props.at("p1")) & bdd_ithvar(nnf_formula->props.at("p2")) & !bdd_ithvar(nnf_formula->props.at("p3")) & !bdd_ithvar(nnf_formula->props.at("p4")) & !bdd_ithvar(nnf_formula->props.at("p5")) & !bdd_ithvar(nnf_formula->props.at("p6"));
+ reset.push_back(1);
+ guard.push_back(monitaal::constraint_t::lower_non_strict(1, 1));
+ bdd_edges.push_back(monitaal::bdd_edge_t(0, 0, guard, reset, label));
+ guard.clear();
+ reset.clear();
+
+ label = !bdd_ithvar(nnf_formula->props.at("p1")) & !bdd_ithvar(nnf_formula->props.at("p2")) & bdd_ithvar(nnf_formula->props.at("p3")) & !bdd_ithvar(nnf_formula->props.at("p4")) & !bdd_ithvar(nnf_formula->props.at("p5")) & !bdd_ithvar(nnf_formula->props.at("p6"));
+ reset.push_back(1);
+ guard.push_back(monitaal::constraint_t::lower_non_strict(1, 1));
+ bdd_edges.push_back(monitaal::bdd_edge_t(0, 0, guard, reset, label));
+ guard.clear();
+ reset.clear();
+
+ label = !bdd_ithvar(nnf_formula->props.at("p1")) & !bdd_ithvar(nnf_formula->props.at("p2")) & !bdd_ithvar(nnf_formula->props.at("p3")) & bdd_ithvar(nnf_formula->props.at("p4")) & !bdd_ithvar(nnf_formula->props.at("p5")) & !bdd_ithvar(nnf_formula->props.at("p6"));
+ reset.push_back(1);
+ guard.push_back(monitaal::constraint_t::lower_non_strict(1, 1));
+ bdd_edges.push_back(monitaal::bdd_edge_t(0, 0, guard, reset, label));
+ guard.clear();
+ reset.clear();
- label = bdd_true();
+ label = !bdd_ithvar(nnf_formula->props.at("p1")) & !bdd_ithvar(nnf_formula->props.at("p2")) & !bdd_ithvar(nnf_formula->props.at("p3")) & !bdd_ithvar(nnf_formula->props.at("p4")) & bdd_ithvar(nnf_formula->props.at("p5")) & !bdd_ithvar(nnf_formula->props.at("p6"));
+ reset.push_back(1);
+ guard.push_back(monitaal::constraint_t::lower_non_strict(1, 1));
+ bdd_edges.push_back(monitaal::bdd_edge_t(0, 0, guard, reset, label));
+ guard.clear();
+ reset.clear();
+ label = !bdd_ithvar(nnf_formula->props.at("p1")) & !bdd_ithvar(nnf_formula->props.at("p2")) & !bdd_ithvar(nnf_formula->props.at("p3")) & !bdd_ithvar(nnf_formula->props.at("p4")) & !bdd_ithvar(nnf_formula->props.at("p5")) & bdd_ithvar(nnf_formula->props.at("p6"));
+ reset.push_back(1);
+ guard.push_back(monitaal::constraint_t::lower_non_strict(1, 1));
bdd_edges.push_back(monitaal::bdd_edge_t(0, 0, guard, reset, label));
+ guard.clear();
+ reset.clear();
model = monitaal::TAwithBDDEdges(name, clocks, locations, bdd_edges, 0); // last arg: initial location id
clocks.clear();
locations.clear();
bdd_edges.clear();
+
if (out_format.has_value() && !out_flatten) {
if (out_format.value()) {
@@ -1754,7 +1793,79 @@
out_str << "location:" << "M" << ":ell_0{initial: : labels: accept_M}" << std::endl;
- out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter << " : do: turn = 0; ";
+ out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter
+ << " && p_" << std::to_string(nnf_formula->props.at("p1")) << " >= 1"
+ << " && p_" << std::to_string(nnf_formula->props.at("p2")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p3")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p4")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p5")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p6")) << " % 2 == 0"
+ << " && x >= 1 : do: x = 0; turn = 0; ";
+ for (auto i = 0; i < num_all_props; ++i) {
+ out_str << "p_" << i + 1 << " = 2" << (i == num_all_props - 1 ? "" : "; ");
+ }
+ out_str << "}" << std::endl;
+
+ out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter
+ << " && p_" << std::to_string(nnf_formula->props.at("p1")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p2")) << " >= 1"
+ << " && p_" << std::to_string(nnf_formula->props.at("p3")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p4")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p5")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p6")) << " % 2 == 0"
+ << " && x >= 1 : do: x = 0; turn = 0; ";
+ for (auto i = 0; i < num_all_props; ++i) {
+ out_str << "p_" << i + 1 << " = 2" << (i == num_all_props - 1 ? "" : "; ");
+ }
+ out_str << "}" << std::endl;
+
+ out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter
+ << " && p_" << std::to_string(nnf_formula->props.at("p1")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p2")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p3")) << " >= 1"
+ << " && p_" << std::to_string(nnf_formula->props.at("p4")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p5")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p6")) << " % 2 == 0"
+ << " && x >= 1 : do: x = 0; turn = 0; ";
+ for (auto i = 0; i < num_all_props; ++i) {
+ out_str << "p_" << i + 1 << " = 2" << (i == num_all_props - 1 ? "" : "; ");
+ }
+ out_str << "}" << std::endl;
+
+ out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter
+ << " && p_" << std::to_string(nnf_formula->props.at("p1")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p2")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p3")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p4")) << " >= 1"
+ << " && p_" << std::to_string(nnf_formula->props.at("p5")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p6")) << " % 2 == 0"
+ << " && x >= 1 : do: x = 0; turn = 0; ";
+ for (auto i = 0; i < num_all_props; ++i) {
+ out_str << "p_" << i + 1 << " = 2" << (i == num_all_props - 1 ? "" : "; ");
+ }
+ out_str << "}" << std::endl;
+
+ out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter
+ << " && p_" << std::to_string(nnf_formula->props.at("p1")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p2")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p3")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p4")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p5")) << " >= 1"
+ << " && p_" << std::to_string(nnf_formula->props.at("p6")) << " % 2 == 0"
+ << " && x >= 1 : do: x = 0; turn = 0; ";
+ for (auto i = 0; i < num_all_props; ++i) {
+ out_str << "p_" << i + 1 << " = 2" << (i == num_all_props - 1 ? "" : "; ");
+ }
+ out_str << "}" << std::endl;
+
+ out_str << "edge:" << "M" << ":ell_0:ell_0:a{provided: g == 0 && turn == " << components_counter
+ << " && p_" << std::to_string(nnf_formula->props.at("p1")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p2")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p3")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p4")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p5")) << " % 2 == 0"
+ << " && p_" << std::to_string(nnf_formula->props.at("p6")) << " >= 1"
+ << " && x >= 1 : do: x = 0; turn = 0; ";
for (auto i = 0; i < num_all_props; ++i) {
out_str << "p_" << i + 1 << " = 2" << (i == num_all_props - 1 ? "" : "; ");
}