Functions
op_ex_synthesis.cpp File Reference
Tutorials

Tutorial, synthesis of natural projections with certain properties. More...

#include <stdio.h>
#include <iostream>
#include <libfaudes.h>

Go to the source code of this file.

Functions

int main (int argc, char *argv[])
 

Detailed Description

Tutorial, synthesis of natural projections with certain properties.

Thie tutorial describes the computation of a natural projection that is

  • an Lm-observer
  • an Lm-observer and locally control consistent (LCC)
  • an Lm-observer and output control consistent (OCC) The resulting abstractions also illustrate that the respective conditions imply each other: Lm-observer and OCC => Lm-observer and LCC => Lm-observer
/** @file op_ex_synthesis.cpp
Tutorial, synthesis of natural projections with certain properties.
Thie tutorial describes the computation of a natural projection that is
- an Lm-observer
- an Lm-observer and locally control consistent (LCC)
- an Lm-observer and output control consistent (OCC)
The resulting abstractions also illustrate that the respective conditions imply each other:
Lm-observer and OCC => Lm-observer and LCC => Lm-observer
@ingroup Tutorials
@include op_ex_synthesis.cpp
*/
#include <stdio.h>
#include <iostream>
#include <libfaudes.h>
// make libFAUDES namespace available
using namespace faudes;
int main(int argc, char* argv[]) {
/////////////////////////////
//Synthesis of an Lm-observer
/////////////////////////////
// construct original Generator from file
System genOrig = System("data/ex_synthesis/ex_natural_all.gen");
genOrig.GraphWrite("data/ex_synthesis/ex_natural_all.png");
// construct initial abstraction alphabet from file
EventSet highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
// compute an abstraction that is an Lm-observer while keeping the events in the original abstraction alphabet
EventSet newHighAlph;
System genClosed(genOrig);
Generator genDyn;
// compute closed observer
calcClosedObserver(genClosed,highAlph);
System genClosedProj;
aProject(genClosed,highAlph,genClosedProj);
genClosedProj.Write("data/ex_synthesis/ex_natural_closed_proj.gen");
genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_closed_proj.png");
// compute natural observer
highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
calcNaturalObserver(genClosed,highAlph);
highAlph.Write();
aProject(genClosed,highAlph,genClosedProj);
genClosedProj.Write("data/ex_synthesis/ex_natural_obs_proj.gen");
genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_obs_proj.png");
//genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_obs_proj.svg");
// MSA-observer
highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
System genMSA(genOrig);
Generator genDynMSA;
// compute natural observer
calcMSAObserver(genClosed,highAlph);
highAlph.Write();
aProject(genClosed,highAlph,genClosedProj);
genClosedProj.Write("data/ex_synthesis/ex_natural_msa_proj.gen");
genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_msa_proj.png");
// Natural observer with LCC
highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
System genLCC(genOrig);
Generator genDynLCC;
EventSet controllableEvents;
//controllableEvents.Insert("gamma");
controllableEvents.Insert("a");
controllableEvents.Insert("f");
controllableEvents.Insert("g");
controllableEvents.Insert("h");
// compute natural observer with lcc
calcNaturalObserverLCC(genLCC,controllableEvents, highAlph);
highAlph.Write();
aProject(genLCC,highAlph,genClosedProj);
genClosedProj.Write("data/ex_synthesis/ex_natural_obslcc_proj.gen");
genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_obslcc_proj.png");
// MSA observer with LCC
highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
genDynLCC.Clear();
// compute natural observer with lcc
calcMSAObserverLCC(genLCC,controllableEvents, highAlph);
highAlph.Write();
aProject(genLCC,highAlph,genClosedProj);
genClosedProj.Write("data/ex_synthesis/ex_natural_msalcc_proj.gen");
genClosedProj.GraphWrite("data/ex_synthesis/ex_natural_msalcc_proj.png");
// ========================================================
// Observer comptations with event relabeling
// ========================================================
genOrig = System("data/ex_synthesis/ex_relabel_all.gen");
genOrig.GraphWrite("data/ex_synthesis/ex_relabel_all.png");
System genObs(genOrig);
std::map< Idx, std::set< Idx > > mapRelabeledEvents;
highAlph = EventSet("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
calcAbstAlphClosed(genObs, highAlph, newHighAlph, mapRelabeledEvents);
// Write the resulting generator and the new high-level alphabet to a file
genObs.Write("data/ex_synthesis/ex_relabel_closed_result.gen");
genObs.GraphWrite("data/ex_synthesis/ex_relabel_closed_result.png");
newHighAlph.Write("data/ex_synthesis/ex_relabel_closed_result.alph");
// evaluate the natural projection for the resulting generator and high-level alphabet
System genHigh;
aProject(genObs, newHighAlph, genHigh);
// Write the high-level generator to a file
genHigh.Write("data/ex_synthesis/ex_relabel_closed_high.gen");
genHigh.GraphWrite("data/ex_synthesis/ex_relabel_closed_high.png");
std::cout << "##########################################################################\n";
std::cout << "# Lm-observer computed; the result can be found in the folder./results/ex_synthesis\n";
std::cout << "##########################################################################\n";
//////////////////////////////////////////////////////////////////////////////////
// Synthesis of a natural projection that fulfills local control consistency (LCC)
//////////////////////////////////////////////////////////////////////////////////
// read the oritinal generator and high-level alphabetd from file input
genObs = genOrig;
highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
// compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
newHighAlph.Clear();
mapRelabeledEvents.clear();
calcAbstAlphObs(genObs, highAlph, newHighAlph, mapRelabeledEvents);
genObs.Write("data/ex_synthesis/ex_relabel_obs_result.gen");
genObs.GraphWrite("data/ex_synthesis/ex_relabel_obs_result.png");
newHighAlph.Write("data/ex_synthesis/ex_relabel_obs_result.alph");
// evaluate the natural projection for the resulting generator and high-level alphabet
aProject(genObs, newHighAlph, genHigh);
// Write the high-level generator to a file
genHigh.Write("data/ex_synthesis/ex_relabel_obs_high.gen");
genHigh.GraphWrite("data/ex_synthesis/ex_relabel_obs_high.png");
std::cout << "################################################################################\n";
std::cout << "# Lm-observer computed; the result can be found in the folder./results/ex_synthesis\n";
std::cout << "################################################################################\n";
//////////////////////////////////////////////////////////////////////////////////
// Synthesis of a natural projection that fulfills local control consistency (LCC)
//////////////////////////////////////////////////////////////////////////////////
// read the oritinal generator and high-level alphabetd from file input
genObs = genOrig;
highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
// compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
newHighAlph.Clear();
mapRelabeledEvents.clear();
calcAbstAlphMSA(genObs, highAlph, newHighAlph, mapRelabeledEvents);
genObs.Write("data/ex_synthesis/ex_relabel_msa_result.gen");
genObs.GraphWrite("data/ex_synthesis/ex_relabel_msa_result.png");
newHighAlph.Write("data/ex_synthesis/ex_relabel_msa_result.alph");
// evaluate the natural projection for the resulting generator and high-level alphabet
aProject(genObs, newHighAlph, genHigh);
// Write the high-level generator to a file
genHigh.Write("data/ex_synthesis/ex_relabel_msa_high.gen");
genHigh.GraphWrite("data/ex_synthesis/ex_relabel_msa_high.png");
std::cout << "################################################################################\n";
std::cout << "# MSA-observer omputed; the result can be found in the folder./results/ex_synthesis\n";
std::cout << "################################################################################\n";
//////////////////////////////////////////////////////////////////////////////////
// Synthesis of a natural projection that fulfills local control consistency (LCC) with relabeling
//////////////////////////////////////////////////////////////////////////////////
// read the oritinal generator and high-level alphabetd from file input
genObs = genOrig;
highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
// compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
newHighAlph.Clear();
mapRelabeledEvents.clear();
calcAbstAlphObsLCC(genObs, highAlph, newHighAlph, mapRelabeledEvents);
genObs.Write("data/ex_synthesis/ex_relabel_obslcc_result.gen");
genObs.GraphWrite("data/ex_synthesis/ex_relabel_obslcc_result.png");
newHighAlph.Write("data/ex_synthesis/ex_relabel_obslcc_result.alph");
// evaluate the natural projection for the resulting generator and high-level alphabet
aProject(genObs, newHighAlph, genHigh);
// Write the high-level generator to a file
genHigh.Write("data/ex_synthesis/ex_relabel_obslcc_high.gen");
genHigh.GraphWrite("data/ex_synthesis/ex_relabel_obslcc_high.png");
std::cout << "################################################################################\n";
std::cout << "# Lm-observer with LCC computed; the result can be found in the folder./results/ex_synthesis\n";
std::cout << "################################################################################\n";
//////////////////////////////////////////////////////////////////////////////////
// Synthesis of a natural projection that fulfills local control consistency (LCC)
//////////////////////////////////////////////////////////////////////////////////
// read the oritinal generator and high-level alphabetd from file input
genObs = genOrig;
highAlph.Read("data/ex_synthesis/ex_natural_all.alph", "Alphabet");
// compute an abstraction that is an Lm-observer and LCC whilc keeping the events in the original abstraction alphabet
newHighAlph.Clear();
mapRelabeledEvents.clear();
calcAbstAlphMSALCC(genObs, highAlph, newHighAlph, mapRelabeledEvents);
genObs.Write("data/ex_synthesis/ex_relabel_msalcc_result.gen");
genObs.GraphWrite("data/ex_synthesis/ex_relabel_msalcc_result.png");
newHighAlph.Write("data/ex_synthesis/ex_relabel_msalcc_result.alph");
// evaluate the natural projection for the resulting generator and high-level alphabet
aProject(genObs, newHighAlph, genHigh);
// Write the high-level generator to a file
genHigh.Write("data/ex_synthesis/ex_relabel_msalcc_high.gen");
genHigh.GraphWrite("data/ex_synthesis/ex_relabel_msalcc_high.png");
std::cout << "################################################################################\n";
std::cout << "# MSA-observer with LCC computed; the result can be found in the folder./results/ex_synthesis\n";
std::cout << "################################################################################\n";
return 0;
}
faudes::NameSet::Insert
bool Insert(const Idx &rIndex)
Add an element by index.
Definition: cfl_nameset.cpp:256
main
int main(int argc, char *argv[])
Definition: flxinstall.cpp:1723
faudes::EventSet
NameSet EventSet
Convenience typedef for plain event sets.
Definition: cfl_nameset.h:531
faudes::Generator
vGenerator Generator
Plain generator, api typedef for generator with no attributes.
Definition: cfl_generator.h:3240
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

Definition in file op_ex_synthesis.cpp.

Function Documentation

◆ main()

int main ( int  argc,
char *  argv[] 
)

Definition at line 25 of file op_ex_synthesis.cpp.

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

>>