op_ex_synthesis.cpp
Go to the documentation of this file.
1 /** @file op_ex_synthesis.cpp
2 
3 Tutorial, synthesis of natural projections with certain properties.
4 
5 Thie tutorial describes the computation of a natural projection that is
6  - an Lm-observer
7  - an Lm-observer and locally control consistent (LCC)
8  - an Lm-observer and output control consistent (OCC)
9 The resulting abstractions also illustrate that the respective conditions imply each other:
10 Lm-observer and OCC => Lm-observer and LCC => Lm-observer
11 
12 @ingroup Tutorials
13 
14 @include op_ex_synthesis.cpp
15 */
16 
17 #include <stdio.h>
18 #include <iostream>
19 #include <libfaudes.h>
20 
21 
22 // make libFAUDES namespace available
23 using namespace faudes;
24 
25 int main(int argc, char* argv[]) {
26  /////////////////////////////
27  //Synthesis of an Lm-observer
28  /////////////////////////////
29 
30  // construct original Generator from file
31  System genOrig = System("data/ex_synthesis/ex_natural_all.gen");
32  genOrig.GraphWrite("data/ex_synthesis/ex_natural_all.png");
33  // construct initial abstraction alphabet from file
34  EventSet highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
35  // compute an abstraction that is an Lm-observer while keeping the events in the original abstraction alphabet
36  EventSet newHighAlph;
37  System genClosed(genOrig);
38  Generator genDyn;
39  // compute closed observer
40  calcClosedObserver(genClosed,highAlph);
41  System genClosedProj;
42  aProject(genClosed,highAlph,genClosedProj);
43  genClosedProj.Write("data/ex_synthesis/ex_natural_closed_proj.gen");
44  genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_closed_proj.png");
45  // compute natural observer
46  highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
47  calcNaturalObserver(genClosed,highAlph);
48  highAlph.Write();
49  aProject(genClosed,highAlph,genClosedProj);
50  genClosedProj.Write("data/ex_synthesis/ex_natural_obs_proj.gen");
51  genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_obs_proj.png");
52  //genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_obs_proj.svg");
53 
54  // MSA-observer
55  highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
56  System genMSA(genOrig);
57  Generator genDynMSA;
58  // compute natural observer
59  calcMSAObserver(genClosed,highAlph);
60  highAlph.Write();
61  aProject(genClosed,highAlph,genClosedProj);
62  genClosedProj.Write("data/ex_synthesis/ex_natural_msa_proj.gen");
63  genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_msa_proj.png");
64 
65  // Natural observer with LCC
66  highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
67  System genLCC(genOrig);
68  Generator genDynLCC;
69  EventSet controllableEvents;
70  //controllableEvents.Insert("gamma");
71  controllableEvents.Insert("a");
72  controllableEvents.Insert("f");
73  controllableEvents.Insert("g");
74  controllableEvents.Insert("h");
75  // compute natural observer with lcc
76  calcNaturalObserverLCC(genLCC,controllableEvents, highAlph);
77  highAlph.Write();
78  aProject(genLCC,highAlph,genClosedProj);
79  genClosedProj.Write("data/ex_synthesis/ex_natural_obslcc_proj.gen");
80  genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_obslcc_proj.png");
81 
82  // MSA observer with LCC
83  highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
84  genDynLCC.Clear();
85  // compute natural observer with lcc
86  calcMSAObserverLCC(genLCC,controllableEvents, highAlph);
87  highAlph.Write();
88  aProject(genLCC,highAlph,genClosedProj);
89  genClosedProj.Write("data/ex_synthesis/ex_natural_msalcc_proj.gen");
90  genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_msalcc_proj.png");
91 
92 
93  // ========================================================
94  // Observer comptations with event relabeling
95  // ========================================================
96  genOrig = System("data/ex_synthesis/ex_relabel_all.gen");
97  genOrig.GraphWrite("data/ex_synthesis/ex_relabel_all.png");
98  System genObs(genOrig);
99  std::map< Idx, std::set< Idx > > mapRelabeledEvents;
100  highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
101  calcAbstAlphClosed(genObs, highAlph, newHighAlph, mapRelabeledEvents);
102  // Write the resulting generator and the new high-level alphabet to a file
103  genObs.Write("data/ex_synthesis/ex_relabel_closed_result.gen");
104  genObs.GraphWrite("data/ex_synthesis/ex_relabel_closed_result.png");
105  newHighAlph.Write("data/ex_synthesis/ex_relabel_closed_result.alph");
106  // evaluate the natural projection for the resulting generator and high-level alphabet
107  System genHigh;
108  aProject(genObs, newHighAlph, genHigh);
109  // Write the high-level generator to a file
110  genHigh.Write("data/ex_synthesis/ex_relabel_closed_high.gen");
111  genHigh.GraphWrite("data/ex_synthesis/ex_relabel_closed_high.png");
112  std::cout << "##########################################################################\n";
113  std::cout << "# Lm-observer computed; the result can be found in the folder./results/ex_synthesis\n";
114  std::cout << "##########################################################################\n";
115 
116  //////////////////////////////////////////////////////////////////////////////////
117  // Synthesis of a natural projection that fulfills local control consistency (LCC)
118  //////////////////////////////////////////////////////////////////////////////////
119 
120  // read the oritinal generator and high-level alphabetd from file input
121  genObs = genOrig;
122  highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
123  // compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
124  newHighAlph.Clear();
125  mapRelabeledEvents.clear();
126  calcAbstAlphObs(genObs, highAlph, newHighAlph, mapRelabeledEvents);
127  genObs.Write("data/ex_synthesis/ex_relabel_obs_result.gen");
128  genObs.GraphWrite("data/ex_synthesis/ex_relabel_obs_result.png");
129  newHighAlph.Write("data/ex_synthesis/ex_relabel_obs_result.alph");
130  // evaluate the natural projection for the resulting generator and high-level alphabet
131  aProject(genObs, newHighAlph, genHigh);
132  // Write the high-level generator to a file
133  genHigh.Write("data/ex_synthesis/ex_relabel_obs_high.gen");
134  genHigh.GraphWrite("data/ex_synthesis/ex_relabel_obs_high.png");
135  std::cout << "################################################################################\n";
136  std::cout << "# Lm-observer computed; the result can be found in the folder./results/ex_synthesis\n";
137  std::cout << "################################################################################\n";
138 
139  //////////////////////////////////////////////////////////////////////////////////
140  // Synthesis of a natural projection that fulfills local control consistency (LCC)
141  //////////////////////////////////////////////////////////////////////////////////
142 
143  // read the oritinal generator and high-level alphabetd from file input
144  genObs = genOrig;
145  highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
146  // compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
147  newHighAlph.Clear();
148  mapRelabeledEvents.clear();
149  calcAbstAlphMSA(genObs, highAlph, newHighAlph, mapRelabeledEvents);
150  genObs.Write("data/ex_synthesis/ex_relabel_msa_result.gen");
151  genObs.GraphWrite("data/ex_synthesis/ex_relabel_msa_result.png");
152  newHighAlph.Write("data/ex_synthesis/ex_relabel_msa_result.alph");
153  // evaluate the natural projection for the resulting generator and high-level alphabet
154  aProject(genObs, newHighAlph, genHigh);
155  // Write the high-level generator to a file
156  genHigh.Write("data/ex_synthesis/ex_relabel_msa_high.gen");
157  genHigh.GraphWrite("data/ex_synthesis/ex_relabel_msa_high.png");
158  std::cout << "################################################################################\n";
159  std::cout << "# MSA-observer omputed; the result can be found in the folder./results/ex_synthesis\n";
160  std::cout << "################################################################################\n";
161 
162 
163  //////////////////////////////////////////////////////////////////////////////////
164  // Synthesis of a natural projection that fulfills local control consistency (LCC) with relabeling
165  //////////////////////////////////////////////////////////////////////////////////
166 
167  // read the oritinal generator and high-level alphabetd from file input
168  genObs = genOrig;
169  highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
170  // compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
171  newHighAlph.Clear();
172  mapRelabeledEvents.clear();
173  calcAbstAlphObsLCC(genObs, highAlph, newHighAlph, mapRelabeledEvents);
174  genObs.Write("data/ex_synthesis/ex_relabel_obslcc_result.gen");
175  genObs.GraphWrite("data/ex_synthesis/ex_relabel_obslcc_result.png");
176  newHighAlph.Write("data/ex_synthesis/ex_relabel_obslcc_result.alph");
177  // evaluate the natural projection for the resulting generator and high-level alphabet
178  aProject(genObs, newHighAlph, genHigh);
179  // Write the high-level generator to a file
180  genHigh.Write("data/ex_synthesis/ex_relabel_obslcc_high.gen");
181  genHigh.GraphWrite("data/ex_synthesis/ex_relabel_obslcc_high.png");
182  std::cout << "################################################################################\n";
183  std::cout << "# Lm-observer with LCC computed; the result can be found in the folder./results/ex_synthesis\n";
184  std::cout << "################################################################################\n";
185 
186  //////////////////////////////////////////////////////////////////////////////////
187  // Synthesis of a natural projection that fulfills local control consistency (LCC)
188  //////////////////////////////////////////////////////////////////////////////////
189 
190  // read the oritinal generator and high-level alphabetd from file input
191  genObs = genOrig;
192  highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
193  // compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
194  newHighAlph.Clear();
195  mapRelabeledEvents.clear();
196  calcAbstAlphMSALCC(genObs, highAlph, newHighAlph, mapRelabeledEvents);
197  genObs.Write("data/ex_synthesis/ex_relabel_msalcc_result.gen");
198  genObs.GraphWrite("data/ex_synthesis/ex_relabel_msalcc_result.png");
199  newHighAlph.Write("data/ex_synthesis/ex_relabel_msalcc_result.alph");
200  // evaluate the natural projection for the resulting generator and high-level alphabet
201  aProject(genObs, newHighAlph, genHigh);
202  // Write the high-level generator to a file
203  genHigh.Write("data/ex_synthesis/ex_relabel_msalcc_high.gen");
204  genHigh.GraphWrite("data/ex_synthesis/ex_relabel_msalcc_high.png");
205  std::cout << "################################################################################\n";
206  std::cout << "# MSA-observer with LCC computed; the result can be found in the folder./results/ex_synthesis\n";
207  std::cout << "################################################################################\n";
208 
209  return 0;
210 }
faudes::NameSet
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
faudes::NameSet::Insert
bool Insert(const Idx &rIndex)
Add an element by index.
Definition: cfl_nameset.cpp:256
faudes::TcGenerator
Generator with controllability attributes.
Definition: cfl_cgenerator.h:273
faudes::Type::Read
void Read(const std::string &rFileName, const std::string &rLabel="", const Type *pContext=0)
Read configuration data from file with label specified.
Definition: cfl_types.cpp:261
faudes::Type::Write
void Write(const Type *pContext=0) const
Write configuration data to console.
Definition: cfl_types.cpp:139
faudes::vGenerator
Base class of all FAUDES generators.
Definition: cfl_generator.h:213
faudes::vGenerator::GraphWrite
void GraphWrite(const std::string &rFileName, const std::string &rOutFormat="", const std::string &rDotExec="dot") const
Produce graphical representation of this generator.
Definition: cfl_generator.cpp:3847
faudes::vGenerator::Clear
virtual void Clear(void)
Clear generator data.
Definition: cfl_generator.cpp:582
faudes::TBaseSet::Clear
virtual void Clear(void)
Clear all set.
Definition: cfl_baseset.h:1902
faudes::EventSet
NameSet EventSet
Convenience typedef for plain event sets.
Definition: cfl_nameset.h:531
faudes::System
TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid > System
Convenience typedef for std System.
Definition: cfl_cgenerator.h:913
faudes::aProject
void aProject(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen)
Deterministic projection.
Definition: cfl_project.cpp:1417
faudes::calcAbstAlphObsLCC
void calcAbstAlphObsLCC(System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
Lm-observer computation including local control consistency (LCC).
Definition: op_observercomputation.cpp:1171
faudes::calcAbstAlphObs
void calcAbstAlphObs(System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
Lm-observer computation.
Definition: op_observercomputation.cpp:746
faudes::calcAbstAlphMSA
void calcAbstAlphMSA(System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
MSA-observer computation.
Definition: op_observercomputation.cpp:825
faudes::calcMSAObserverLCC
Int calcMSAObserverLCC(const Generator &rGen, const EventSet &rControllableEvents, EventSet &rHighAlph)
MSA-observer computation including local control consistency (LCC) by adding events to the high-level...
Definition: op_observercomputation.cpp:497
faudes::calcAbstAlphClosed
void calcAbstAlphClosed(System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
L(G)-observer computation.
Definition: op_observercomputation.cpp:667
faudes::calcClosedObserver
Idx calcClosedObserver(const Generator &rGen, EventSet &rHighAlph)
L(G)-observer computation by adding events to the high-level alphabet.
Definition: op_observercomputation.cpp:413
faudes::calcAbstAlphMSALCC
void calcAbstAlphMSALCC(System &rGenObs, EventSet &rHighAlph, EventSet &rNewHighAlph, map< Idx, set< Idx > > &rMapRelabeledEvents)
MSA-observer computation including local control consistency (LCC).
Definition: op_observercomputation.cpp:1245
faudes::calcNaturalObserverLCC
Int calcNaturalObserverLCC(const Generator &rGen, const EventSet &rControllableEvents, EventSet &rHighAlph)
Lm(G)-observer computation including local control consistency (LCC) by adding events to the high-lev...
Definition: op_observercomputation.cpp:454
faudes::calcNaturalObserver
Int calcNaturalObserver(const Generator &rGen, EventSet &rHighAlph)
Lm(G)-observer computation by adding events to the high-level alphabet.
Definition: op_observercomputation.cpp:433
faudes::calcMSAObserver
Int calcMSAObserver(const Generator &rGen, EventSet &rHighAlph)
MSA-observer computation by adding events to the high-level alphabet.
Definition: op_observercomputation.cpp:476
libfaudes.h
Includes all libFAUDES headers, incl plugings
faudes
libFAUDES resides within the namespace faudes.
Definition: cfl_agenerator.h:43
main
int main(int argc, char *argv[])
Definition: op_ex_synthesis.cpp:25

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

>>