|
|
||||||
|
#include "libfaudes.h" Go to the source code of this file.
Detailed Description
Tutorial, I/O system synthesis This tutorial runs the two examples from the techical report Moor/Schmidt/Wittmann, 2010. It thereby demonstrates the use of the provided functions for the synthesis of I/O controllers. /** @file ios_2_synthesis.cpp
Tutorial, I/O system synthesis
This tutorial runs the two examples from
the techical report Moor/Schmidt/Wittmann, 2010.
It thereby demonstrates the use of the provided
functions for the synthesis of I/O controllers.
@ingroup Tutorials
@include ios_2_synthesis.cpp
*/
#include "libfaudes.h"
// make the faudes namespace available to our program
using namespace faudes;
/////////////////
// main program
/////////////////
int main() {
// Read plant and speification generators
IoSystem planta("data/ios_planta.gen");
Generator speca("data/ios_speca.gen");
// Adjust specification alphabet
InvProject(speca,planta.Alphabet());
// Run synthesis algorithm
IoSystem supera;
supera.StateNamesEnabled(false);
IoSynthesis(planta,speca,supera);
aStateMin(supera,supera);
// Report to console
std::cout << "################################\n";
std::cout << "# tutorial, supervisor a \n";
supera.DWrite();
std::cout << "################################\n";
// Read plant and speification generators
IoSystem plantb("data/ios_plantb.gen");
Generator specb("data/ios_specb.gen");
// Adjust specification alphabet
InvProject(specb,plantb.Alphabet());
// Run synthesis algorithm
IoSystem superb;
superb.StateNamesEnabled(false);
IoSynthesisNB(plantb,specb,superb);
aStateMin(superb,superb);
// Report to console
std::cout << "################################\n";
std::cout << "# tutorial, supervisor b \n";
superb.DWrite();
std::cout << "################################\n";
// Record testcase
FAUDES_TEST_DUMP("supA",supera);
FAUDES_TEST_DUMP("supB",superb);
// Done
return 0;
}
#define FAUDES_TEST_DUMP(mes, dat) Test protocol record macro ("mangle" filename for platform independance) Definition: cfl_helper.h:483 vGenerator Generator Plain generator, api typedef for generator with no attributes. Definition: cfl_generator.h:3240 void aStateMin(const Generator &rGen, Generator &rResGen) State set minimization. Definition: cfl_statemin.cpp:629 void InvProject(Generator &rGen, const EventSet &rProjectAlphabet) Inverse projection. Definition: cfl_project.cpp:1479 Includes all libFAUDES headers, incl plugings TioGenerator< AttributeVoid, AttributeIosState, AttributeIosEvent, AttributeVoid > IoSystem Definition: ios_system.h:777 void IoSynthesisNB(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup) IO system synthesis. Definition: ios_algorithms.cpp:406 void IoSynthesis(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup) IO system synthesis. Definition: ios_algorithms.cpp:420 Definition in file ios_2_synthesis.cpp. Function Documentation◆ main()
Definition at line 29 of file ios_2_synthesis.cpp. libFAUDES 2.32b --- 2024.03.01 --- c++ api documentaion by doxygen |