ios_2_synthesis.cpp File Reference


More...

#include "libfaudes.h"

Go to the source code of this file.

Functions

int main ()
 

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
int main(int argc, char *argv[])
vGenerator Generator
Plain generator, api typedef for generator with no attributes.
void aStateMin(const Generator &rGen, Generator &rResGen)
State set minimization.
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
Includes all libFAUDES headers, incl plugings
libFAUDES resides within the namespace faudes.
TioGenerator< AttributeVoid, AttributeIosState, AttributeIosEvent, AttributeVoid > IoSystem
Definition: ios_system.h:777
void IoSynthesisNB(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)
IO system synthesis.
void IoSynthesis(const IoSystem &rPlant, const Generator &rSpec, IoSystem &rSup)
IO system synthesis.

Definition in file ios_2_synthesis.cpp.

Function Documentation

◆ main()

int main ( void  )

Definition at line 29 of file ios_2_synthesis.cpp.

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