|
|
||||||
|
Tutorial, coordination control. More... #include "libfaudes.h" Go to the source code of this file.
Detailed DescriptionTutorial, coordination control. /** @file con_1_simple.cpp
Tutorial, coordination control
@ingroup Tutorials
@include con_1_simple.cpp
*/
#include "libfaudes.h"
// we make the faudes namespace available to our program
using namespace faudes;
/////////////////
// main program
/////////////////
System g1, g2, g3, gk, spec, plant;
EventSet e1, e2, e3, ek, ec;
EventSetVector eVector;
GeneratorVector gVector, specV;
g1.Read("data/gen1.gen");
g2.Read("data/gen2.gen");
g3.Read("data/gen3.gen");
spec.Read("data/spec.gen");
gVector.Append(g1);
gVector.Append(g2);
gVector.Append(g3);
aParallel(gVector,plant);
e1.Read("data/e1.alph");
e2.Read("data/e2.alph");
e3.Read("data/e3.alph");
ek.Read("data/ek.alph");
ec.Read("data/ec.alph"); // controllable events
eVector.Append(e1);
eVector.Append(e2);
eVector.Append(e3);
System proof;
bool result1 = IsConditionalDecomposable(spec,eVector,ek,proof);
if (result1) {
std::cout << "The language is conditionally decomposable." << std::endl;
}
else {
std::cout << "The language is not conditionally decomposable." << std::endl
<< "The proof strings are showin in the \'proof\' generator." << std::endl;
}
FAUDES_TEST_DUMP("is cond decomp",result1);
//Coordinator
Project(plant,ek,gk);
//PkK, PikK, i=1,2,3
System PkK, P1kK, P2kK, P3kK;
Project(spec,ek,PkK);
Project(spec,e1+ek,P1kK);
Project(spec,e2+ek,P2kK);
Project(spec,e3+ek,P3kK);
specV.Append(P1kK);
specV.Append(P2kK);
specV.Append(P3kK);
bool result2 = IsConditionalControllable(specV,PkK,gVector,gk,ec);
if (result2) {
std::cout << "The language is conditionally controllable." << std::endl;
}
else {
std::cout << "The language is not conditionally controllable." << std::endl;
}
bool result3 = IsConditionalClosed(specV,PkK,gVector,gk);
FAUDES_TEST_DUMP("is cond ctrl",result2);
if (result3) {
std::cout << "The language is conditionally closed." << std::endl;
}
else {
std::cout << "The language is not conditionally closed." << std::endl;
}
FAUDES_TEST_DUMP("is cond closed",result3);
}
#define FAUDES_TEST_DUMP(mes, dat) Test protocol record macro ("mangle" filename for platform independance) Definition: cfl_helper.h:483 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 bool IsConditionalClosed(const GeneratorVector &specVect, const Generator &pk, const GeneratorVector &genVect, const Generator &gk) Conditionalclosedness Checking Algorithm. Definition: con_closed.cpp:16 bool IsConditionalControllable(const GeneratorVector &specVect, const Generator &pk, const GeneratorVector &genVect, const Generator &gk, const EventSet &ACntrl) Conditionalcontrollability Checking Algorithm. Definition: con_controllability.cpp:16 bool IsConditionalDecomposable(const Generator &gen, const EventSetVector &ee, const EventSet &ek, Generator &proof) Conditionaldecomposability Checking Algorithm. Definition: con_decomposability.cpp:16 TcGenerator< AttributeVoid, AttributeVoid, AttributeCFlags, AttributeVoid > System Convenience typedef for std System. Definition: cfl_cgenerator.h:913 TBaseVector< Generator > GeneratorVector Convenience typedef for vectors og generators. Definition: cfl_generator.h:3246 void aParallel(const Generator &rGen1, const Generator &rGen2, Generator &rResGen) Parallel composition. Definition: cfl_parallel.cpp:51 void Project(const Generator &rGen, const EventSet &rProjectAlphabet, Generator &rResGen) Deterministic projection. Definition: cfl_project.cpp:1349 Includes all libFAUDES headers, incl plugings Definition in file con_1_simple.cpp. Function Documentation◆ main()
Definition at line 20 of file con_1_simple.cpp. libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen |