syn_2_omega.cpp
Go to the documentation of this file.
1 /** @file syn_2_omega.cpp
2 
3 Synthesis for omega languages.
4 
5 @ingroup Tutorials
6 
7 @include syn_2_omega.cpp
8 
9 */
10 
11 #include "libfaudes.h"
12 
13 
14 // we make the faudes namespace available to our program
15 using namespace faudes;
16 
17 
18 /////////////////
19 // main program
20 /////////////////
21 
22 
23 int main() {
24 
25 
26  /////////////////////////////////////////////
27  // Omega control (closed supervisors)
28  //
29  // The A-B-Machine is a machine that can run process A (event a) or process B (event b).
30  // Per operation, the machine may succeed (event c) of fail (event d). However, it is
31  // guaranteed to suceed eventually. We have three variations:
32  //
33  // 1: the std case
34  // 2: process B exhausts the machine: it will succeed in process B once and then
35  // fail on further processes B until process A was run.
36  // 3: process B breaks the machine: it will succeed in process B once and
37  // then fail in any further processes
38  //
39  // We synthesise controllers for 3 variant specifications
40  //
41  // 1. Alternate in successfully processing A and B
42  // 2. Keep on eventually succeeding in some process
43  // 3. Start with process A, eventually switch to B, repeat
44  //
45  /////////////////////////////////////////////
46 
47 
48  // Read A-B-Machines and specifications
49  System machineab1("data/wmachineab1.gen");
50  System machineab2("data/wmachineab2.gen");
51  System machineab3("data/wmachineab3.gen");
52  Generator specab1("data/wspecab1.gen");
53  Generator specab2("data/wspecab2.gen");
54  Generator specab3("data/wspecab3.gen");
55 
56  // Fix lazy specifications by intersection with plant
57  Generator specab11; OmegaProduct(specab1,machineab1,specab11); specab11.OmegaTrim();
58  Generator specab21; OmegaProduct(specab2,machineab1,specab21); specab21.OmegaTrim();
59  Generator specab31; OmegaProduct(specab3,machineab1,specab31); specab31.OmegaTrim();
60  Generator specab12; OmegaProduct(specab1,machineab2,specab12); specab12.OmegaTrim();
61  Generator specab22; OmegaProduct(specab2,machineab2,specab22); specab22.OmegaTrim();
62  Generator specab32; OmegaProduct(specab3,machineab2,specab32); specab32.OmegaTrim();
63  Generator specab13; OmegaProduct(specab1,machineab3,specab13); specab13.OmegaTrim();
64  Generator specab23; OmegaProduct(specab2,machineab3,specab23); specab23.OmegaTrim();
65  Generator specab33; OmegaProduct(specab3,machineab3,specab33); specab33.OmegaTrim();
66 
67  // Report result to console
68  std::cout << "################################\n";
69  std::cout << "# fixed lazy specifications by omega-trim \n# intersection with plant, state count\n";
70  std::cout << " w.r.t a-b-machine 1 (std case): \n ";
71  std::cout << " #" << specab11.Size() << " #" << specab21.Size() << " #" << specab31.Size() << "\n";
72  std::cout << " w.r.t a-b-machine 2 (b exhausts the machine): \n ";
73  std::cout << " #" << specab12.Size() << " #" << specab22.Size() << " #" << specab32.Size() << "\n";
74  std::cout << " w.r.t a-b-machine 3 (b breaks the machine): \n ";
75  std::cout << " #" << specab13.Size() << " #" << specab23.Size() << " #" << specab33.Size() << "\n";
76  std::cout << "################################\n";
77 
78 
79 
80  // Test (relative closedness)
81  bool rcl1_1 = IsRelativelyOmegaClosed(machineab1,specab11);
82  bool rcl2_1 = IsRelativelyOmegaClosed(machineab1,specab21);
83  bool rcl3_1 = IsRelativelyOmegaClosed(machineab1,specab31);
84  bool rcl1_2 = IsRelativelyOmegaClosed(machineab2,specab12);
85  bool rcl2_2 = IsRelativelyOmegaClosed(machineab2,specab22);
86  bool rcl3_2 = IsRelativelyOmegaClosed(machineab2,specab32);
87  bool rcl1_3 = IsRelativelyOmegaClosed(machineab3,specab13);
88  bool rcl2_3 = IsRelativelyOmegaClosed(machineab3,specab23);
89  bool rcl3_3 = IsRelativelyOmegaClosed(machineab3,specab33);
90 
91 
92  // Report result to console
93  std::cout << "################################\n";
94  std::cout << "# omega relative closedness w.r.t. ab-machines\n";
95  std::cout << " w.r.t a-b-machine 1 (std case): \n ";
96  if(rcl1_1) std::cout << " passed "; else std::cout << " failed ";
97  if(rcl2_1) std::cout << " passed "; else std::cout << " failed ";
98  if(rcl3_1) std::cout << " passed "; else std::cout << " failed ";
99  std::cout << "\n";
100  std::cout << " w.r.t a-b-machine 2 (b exhausts the machine): \n ";
101  if(rcl1_2) std::cout << " passed "; else std::cout << " failed ";
102  if(rcl2_2) std::cout << " passed "; else std::cout << " failed ";
103  if(rcl3_2) std::cout << " passed "; else std::cout << " failed ";
104  std::cout << "\n";
105  std::cout << " w.r.t a-b-machine 3 (b breaks the machine): \n ";
106  if(rcl1_3) std::cout << " passed "; else std::cout << " failed ";
107  if(rcl2_3) std::cout << " passed "; else std::cout << " failed ";
108  if(rcl3_3) std::cout << " passed "; else std::cout << " failed ";
109  std::cout << "\n";
110  std::cout << "################################\n";
111 
112  // Record test case
113  FAUDES_TEST_DUMP("RelClosed_1_1",rcl1_1);
114  FAUDES_TEST_DUMP("RelClosed_2_1",rcl2_1);
115  FAUDES_TEST_DUMP("RelClosed_3_1",rcl3_1);
116  FAUDES_TEST_DUMP("RelClosed_1_2",rcl1_2);
117  FAUDES_TEST_DUMP("RelClosed_2_2",rcl2_2);
118  FAUDES_TEST_DUMP("RelClosed_3_2",rcl3_2);
119  FAUDES_TEST_DUMP("RelClosed_1_3",rcl1_3);
120  FAUDES_TEST_DUMP("RelClosed_2_3",rcl2_3);
121  FAUDES_TEST_DUMP("RelClosed_3_3",rcl3_3);
122 
123  // Close specification
124  Generator specab11c=specab11; PrefixClosure(specab11c);
125  Generator specab12c=specab12; PrefixClosure(specab12c);
126  Generator specab21c=specab21; PrefixClosure(specab21c);
127  Generator specab23c=specab23; PrefixClosure(specab23c);
128 
129  // Synthesise supervisors
130  Generator supab11; SupConCmplNB(machineab1,specab11c,supab11);
131  Generator supab21; SupConCmplNB(machineab1,specab21c,supab21);
132  Generator supab12; SupConCmplNB(machineab2,specab12c,supab12);
133  Generator supab23; SupConCmplNB(machineab3,specab23c,supab23);
134 
135  // Report result to console
136  std::cout << "################################\n";
137  std::cout << "# omega synthesis statistics\n";
138  supab11.SWrite();
139  supab12.SWrite();
140  supab21.SWrite();
141  supab23.SWrite();
142  std::cout << "################################\n";
143 
144  // Record test case
145  FAUDES_TEST_DUMP("Sup1_1",supab11);
146  FAUDES_TEST_DUMP("Sup1_2",supab12);
147  FAUDES_TEST_DUMP("Sup2_1",supab21);
148  FAUDES_TEST_DUMP("Sup2_3",supab23);
149 
150 
151  // Test controllability
152  std::cout << "################################\n";
153  std::cout << "# omega controllability:\n";
154  if(IsOmegaControllable(machineab1,supab11))
155  std::cout << "# supervisor11: passed (expected)\n";
156  else
157  std::cout << "# supervisor11: failed (test case error)\n";
158  if(IsOmegaControllable(machineab2,supab12))
159  std::cout << "# supervisor12: passed (expected)\n";
160  else
161  std::cout << "# supervisor12: failed (test case error)\n";
162  if(IsOmegaControllable(machineab1,supab21))
163  std::cout << "# supervisor21: passed (expected)\n";
164  else
165  std::cout << "# supervisor21: failed (test case error)\n";
166  if(IsOmegaControllable(machineab3,supab23))
167  std::cout << "# supervisor23: passed (expected)\n";
168  else
169  std::cout << "# supervisor23: failed (test case error)\n";
170  std::cout << "################################\n";
171 
172 
173  // Prepare graphical output for documentation, I
174  supab11.StateNamesEnabled(false);
175  supab21.StateNamesEnabled(false);
176  supab12.StateNamesEnabled(false);
177  supab23.StateNamesEnabled(false);
178  StateMin(supab11,supab11);
179  StateMin(supab21,supab21);
180  StateMin(supab12,supab12);
181  StateMin(supab23,supab23);
182 
183  // Prepare graphical output for documentation, II
184  machineab1.Write("tmp_syn_2_machineab1.gen");
185  machineab2.Write("tmp_syn_2_machineab2.gen");
186  machineab3.Write("tmp_syn_2_machineab3.gen");
187  specab1.Write("tmp_syn_2_specab1.gen");
188  specab2.Write("tmp_syn_2_specab2.gen");
189  specab3.Write("tmp_syn_2_specab3.gen");
190  supab11.Write("tmp_syn_2_supab11.gen");
191  supab21.Write("tmp_syn_2_supab21.gen");
192  supab12.Write("tmp_syn_2_supab12.gen");
193  supab23.Write("tmp_syn_2_supab23.gen");
194 
195  //Generator prodab22; Product(machineab2,specab22,prodab22);
196  //prod22.Write("tmp_syn_2_prodab22.gen");
197 
198 
199 
200  /////////////////////////////////////////////
201  // Marking supervisor omega control
202  //
203  //
204  ////////////////////////////////////////////
205 
206  // Run the above test cases
207  Generator msupab11; OmegaSupConNB(machineab1,specab1,msupab11);
208  Generator msupab21; OmegaSupConNB(machineab1,specab2,msupab21);
209  Generator msupab31; OmegaSupConNB(machineab1,specab3,msupab31);
210  Generator msupab12; OmegaSupConNB(machineab2,specab1,msupab12);
211  Generator msupab22; OmegaSupConNB(machineab2,specab2,msupab22);
212  Generator msupab32; OmegaSupConNB(machineab2,specab3,msupab32);
213  Generator msupab13; OmegaSupConNB(machineab3,specab1,msupab13);
214  Generator msupab23; OmegaSupConNB(machineab3,specab2,msupab23);
215  Generator msupab33; OmegaSupConNB(machineab3,specab3,msupab33);
216 
217  // Report statistics
218  std::cout << "################################\n";
219  std::cout << "# omega synthesis statistics\n";
220  msupab11.SWrite();
221  msupab21.SWrite();
222  msupab31.SWrite();
223  msupab12.SWrite();
224  msupab22.SWrite();
225  msupab32.SWrite();
226  msupab13.SWrite();
227  msupab23.SWrite();
228  msupab33.SWrite();
229  std::cout << "################################\n";
230 
231 
232  // Record test case
233  FAUDES_TEST_DUMP("OSup1_1",msupab11);
234  FAUDES_TEST_DUMP("OSup2_1",msupab21);
235  FAUDES_TEST_DUMP("OSup3_1",msupab31);
236  FAUDES_TEST_DUMP("OSup1_2",msupab12);
237  FAUDES_TEST_DUMP("OSup2_2",msupab22);
238  FAUDES_TEST_DUMP("OSup3_2",msupab32);
239  FAUDES_TEST_DUMP("OSup1_3",msupab13);
240  FAUDES_TEST_DUMP("OSup2_3",msupab23);
241  FAUDES_TEST_DUMP("OSup3_3",msupab33);
242 
243  // Prepare graphical output for documentation, I
244  msupab11.StateNamesEnabled(false);
245  msupab21.StateNamesEnabled(false);
246  msupab31.StateNamesEnabled(false);
247  msupab12.StateNamesEnabled(false);
248  msupab22.StateNamesEnabled(false);
249  msupab32.StateNamesEnabled(false);
250  msupab13.StateNamesEnabled(false);
251  msupab23.StateNamesEnabled(false);
252  msupab33.StateNamesEnabled(false);
253  StateMin(msupab11,msupab11);
254  StateMin(msupab21,msupab21);
255  StateMin(msupab31,msupab31);
256  StateMin(msupab12,msupab12);
257  StateMin(msupab22,msupab22);
258  StateMin(msupab32,msupab32);
259  StateMin(msupab13,msupab13);
260  StateMin(msupab23,msupab23);
261  StateMin(msupab33,msupab33);
262 
263  // Prepare graphical output II
264  //msupab11.Write("tmp_syn_2_msupab11.gen");
265  //msupab21.Write("tmp_syn_2_msupab21.gen");
266  msupab31.Write("tmp_syn_2_msupab31.gen");
267  //msupab12.Write("tmp_syn_2_msupab12.gen");
268  //msupab22.Write("tmp_syn_2_msupab22.gen");
269  msupab32.Write("tmp_syn_2_msupab32.gen");
270  //msupab13.Write("tmp_syn_2_msupab13.gen");
271  //msupab23.Write("tmp_syn_2_msupab23.gen");
272  msupab33.Write("tmp_syn_2_msupab33.gen");
273 
274 
275  /////////////////////////////////////////////
276  // Debugging/testing examples
277  /////////////////////////////////////////////
278 
279  // Read example plant and spec
280  System ex1plant("data/wplant1.gen");
281  Generator ex1spec("data/wspec1.gen");
282 
283  // Run omega synthesis procedure
284  Generator ex1super;
285  OmegaSupConNB(ex1plant,ex1spec,ex1super);
286  Generator ex1controller;
287  OmegaConNB(ex1plant,ex1spec,ex1controller);
288 
289  // verify
290  bool cntr1 = IsControllable(ex1plant,ex1controller);
291  bool closed1 = IsRelativelyOmegaClosed(ex1plant,ex1controller);
292 
293  // Prepare graphical output for documentation
294  ex1plant.Write("tmp_syn_2_wplant1.gen");
295  ex1spec.Write("tmp_syn_2_wspec1.gen");
296  ex1super.StateNamesEnabled(false);
297  ex1super.Write("tmp_syn_2_wsuper1.gen");
298 
299  // Report result to console
300  std::cout << "################################\n";
301  std::cout << "# extended omega synthesis example 1 \n";
302  ex1super.DWrite();
303  ex1controller.DWrite();
304  std::cout << "prefix controllability: " << cntr1 << std::endl;
305  std::cout << "rel. top. closed: " << closed1 << std::endl;
306  std::cout << "################################\n";
307 
308 
309  // Read example plant and spec
310  System ex2plant("data/wplant2.gen");
311  Generator ex2spec("data/wspec2.gen");
312 
313  // Fix spec alphabet
314  InvProject(ex2spec,ex2plant.Alphabet());
315 
316  // Run omega synthesis procedure
317  Generator ex2super;
318  OmegaSupConNB(ex2plant,ex2spec,ex2super);
319  Generator ex2controller;
320  OmegaConNB(ex2plant,ex2spec,ex2controller);
321 
322  // verify
323  bool cntr2 = IsControllable(ex2plant,ex2controller);
324  bool closed2 = IsRelativelyOmegaClosed(ex2plant,ex2controller);
325 
326  // Report result to console
327  std::cout << "################################\n";
328  std::cout << "# extended omega synthesis example 2 \n";
329  ex2super.DWrite();
330  ex2controller.DWrite();
331  std::cout << "prefix controllability: " << cntr2 << std::endl;
332  std::cout << "rel. top. closed: " << closed2 << std::endl;
333  std::cout << "################################\n";
334 
335  // Prepare graphical aoutput for documentation
336  ex2plant.Write("tmp_syn_2_wplant2.gen");
337  ex2spec.Write("tmp_syn_2_wspec2.gen");
338  ex2super.StateNamesEnabled(false);
339  ex2super.Write("tmp_syn_2_wsuper2.gen");
340 
341  // Read example plant and spec
342  System ex3plant("data/wplant3.gen");
343  Generator ex3spec("data/wspec3.gen");
344 
345  // Run omega synthesis procedure
346  Generator ex3super;
347  OmegaSupConNormNB(ex3plant,ex3spec,ex3super);
348  StateMin(ex3super, ex3super);
349  Generator ex3controller;
350  OmegaConNormNB(ex3plant,ex3spec,ex3controller);
351  StateMin(ex3controller, ex3controller);
352 
353  // verify
354  bool cntr3 = IsControllable(ex3plant,ex3controller);
355  bool closed3 = IsRelativelyOmegaClosed(ex3plant,ex3controller);
356  Generator ex3plant_loc = ex3plant;
357  Generator ex3contr_loc = ex3controller;
358  MarkAllStates(ex3plant_loc);
359  MarkAllStates(ex3contr_loc);
360  bool norm3 = IsNormal(ex3plant_loc,ex3plant.ObservableEvents(),ex3contr_loc);
361 
362 
363  // Report result to console
364  std::cout << "################################\n";
365  std::cout << "# extended omega synthesis example 3 \n";
366  ex3super.DWrite();
367  ex3controller.DWrite();
368  std::cout << "prefix controllability: " << cntr3 << std::endl;
369  std::cout << "prefix normality : " << norm3 << std::endl;
370  std::cout << "rel. top. closed: " << closed3 << std::endl;
371  std::cout << "################################\n";
372 
373  // Prepare graphical aoutput for documentation
374  ex3plant.Write("tmp_syn_2_wplant3.gen");
375  ex3spec.Write("tmp_syn_2_wspec3.gen");
376  ex3super.StateNamesEnabled(false);
377  ex3super.Write("tmp_syn_2_wsuper3.gen");
378  ex3controller.StateNamesEnabled(false);
379  ex3controller.Write("tmp_syn_2_wcontr3.gen");
380 
381  FAUDES_TEST_DUMP("ex1super",ex1super);
382  FAUDES_TEST_DUMP("ex1controller",ex1controller);
383  FAUDES_TEST_DUMP("ex2super",ex2super);
384  FAUDES_TEST_DUMP("ex2controller",ex2controller);
385  FAUDES_TEST_DUMP("ex3super",ex3super);
386  FAUDES_TEST_DUMP("ex3controller",ex3controller);
387 
388  return 0;
389 }
390 
FAUDES_TEST_DUMP
#define FAUDES_TEST_DUMP(mes, dat)
Test protocol record macro ("mangle" filename for platform independance)
Definition: cfl_helper.h:483
faudes::TaGenerator::Alphabet
const TaEventSet< EventAttr > & Alphabet(void) const
Return const reference to alphabet.
Definition: cfl_agenerator.h:1358
faudes::TcGenerator
Generator with controllability attributes.
Definition: cfl_cgenerator.h:273
faudes::TcGenerator::ObservableEvents
EventSet ObservableEvents(void) const
Get EventSet with observable events.
Definition: cfl_cgenerator.h:1239
faudes::Type::DWrite
void DWrite(const Type *pContext=0) const
Write configuration data to console, debugging format.
Definition: cfl_types.cpp:225
faudes::Type::Write
void Write(const Type *pContext=0) const
Write configuration data to console.
Definition: cfl_types.cpp:139
faudes::Type::SWrite
void SWrite(TokenWriter &rTw) const
Write statistics comment to TokenWriter.
Definition: cfl_types.cpp:256
faudes::vGenerator
Base class of all FAUDES generators.
Definition: cfl_generator.h:213
faudes::vGenerator::StateNamesEnabled
bool StateNamesEnabled(void) const
Whether libFAUEDS functions are requested to generate state names.
Definition: cfl_generator.cpp:999
faudes::vGenerator::Size
Idx Size(void) const
Get generator size (number of states)
Definition: cfl_generator.cpp:577
faudes::vGenerator::OmegaTrim
bool OmegaTrim(void)
Make generator omega-trim.
Definition: cfl_generator.cpp:2334
faudes::StateMin
void StateMin(const Generator &rGen, Generator &rResGen)
State set minimization.
Definition: cfl_statemin.cpp:613
faudes::PrefixClosure
void PrefixClosure(Generator &rGen)
Prefix Closure.
Definition: cfl_regular.cpp:950
faudes::MarkAllStates
void MarkAllStates(vGenerator &rGen)
RTI wrapper function.
Definition: cfl_generator.cpp:3986
faudes::OmegaProduct
void OmegaProduct(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Product composition for Buechi automata.
Definition: cfl_omega.cpp:102
faudes::InvProject
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
Definition: cfl_project.cpp:1479
faudes::OmegaConNormNB
void OmegaConNormNB(const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
Omega-synthesis for partial observation (experimental!)
Definition: syn_wsupcon.cpp:1737
faudes::IsControllable
bool IsControllable(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSupCandGen)
Test controllability.
Definition: syn_supcon.cpp:718
faudes::IsNormal
bool IsNormal(const Generator &rL, const EventSet &rOAlph, const Generator &rK)
IsNormal: checks normality of a language K generated by rK wrt a language L generated by rL and the s...
Definition: syn_supnorm.cpp:104
faudes::OmegaSupConNormNB
void OmegaSupConNormNB(const Generator &rPlantGen, const EventSet &rCAlph, const EventSet &rOAlph, const Generator &rSpecGen, Generator &rResGen)
Omega-synthesis for partial observation (experimental!)
Definition: syn_wsupcon.cpp:1695
faudes::IsOmegaControllable
bool IsOmegaControllable(const Generator &rGenPlant, const EventSet &rCAlph, const Generator &rGenCand)
Test omega controllability.
Definition: syn_wsupcon.cpp:42
faudes::IsRelativelyOmegaClosed
bool IsRelativelyOmegaClosed(const Generator &rGenPlant, const Generator &rGenCand)
Test for relative closedness, omega languages.
Definition: syn_functions.cpp:396
faudes::OmegaSupConNB
void OmegaSupConNB(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Omega-synthesis.
Definition: syn_wsupcon.cpp:1588
faudes::SupConCmplNB
void SupConCmplNB(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Supremal controllable and complete sublanguage.
Definition: syn_wsupcon.cpp:209
faudes::OmegaConNB
void OmegaConNB(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Omega-synthesis.
Definition: syn_wsupcon.cpp:1627
libfaudes.h
Includes all libFAUDES headers, incl plugings
faudes
libFAUDES resides within the namespace faudes.
Definition: cfl_agenerator.h:43
main
int main()
Definition: syn_2_omega.cpp:23

libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen

>>