syn_1_simple.cpp
Go to the documentation of this file.
1 /** @file syn_1_simple.cpp
2 
3 Tutorial, std monolitic synthesis.
4 
5 
6 This tutorial uses a very simple example to illustrate the
7 std monolithic controller synthesis
8 as originally proposed by Ramadge and Wonham.
9 
10 
11 @ingroup Tutorials
12 
13 @include syn_1_simple.cpp
14 
15 */
16 
17 #include "libfaudes.h"
18 
19 
20 // we make the faudes namespace available to our program
21 using namespace faudes;
22 
23 
24 
25 
26 /////////////////
27 // main program
28 /////////////////
29 
30 int main() {
31 
32 
33  // Compose plant dynamics from two very simple machines
34  Generator tempgen, machinea, machineb;
35  System cplant;
36 
37  tempgen.Read("data/verysimplemachine.gen");
38  tempgen.Version("1",machinea);
39  tempgen.Version("2",machineb);
40  Parallel(machinea,machineb,cplant);
41 
42  // Declare controllable events
43  EventSet contevents;
44  contevents.Insert("alpha_1");
45  contevents.Insert("alpha_2");
46  cplant.SetControllable(contevents);
47 
48  // Write to file
49  cplant.Write("tmp_cplant12.gen");
50 
51  // Report to console
52  std::cout << "################################\n";
53  std::cout << "# tutorial, plant model \n";
54  cplant.DWrite();
55  std::cout << "################################\n";
56 
57  // Read specification
58  Generator specification;
59  specification.Read("data/buffer.gen");
60  InvProject(specification,cplant.Alphabet());
61  specification.Name("simple machines specification");
62 
63  // Write to file
64  specification.Write("tmp_specification12.gen");
65 
66  // Report to console
67  std::cout << "################################\n";
68  std::cout << "# tutorial, specification \n";
69  specification.DWrite();
70  std::cout << "################################\n";
71 
72  // Run synthesis algorithm
73  System supervisor;
74  SupConNB(cplant,specification,supervisor);
75  supervisor.Name("simple machines supervisor");
76  supervisor.Write("tmp_supervisor12.gen");
77 
78  // Report to console
79  std::cout << "################################\n";
80  std::cout << "# tutorial, supervisor\n";
81  supervisor.DWrite();
82  std::cout << "################################\n";
83 
84  return 0;
85 }
86 
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
bool Insert(const Idx &rIndex)
Add an element by index.
const TaEventSet< EventAttr > & Alphabet(void) const
Return const reference to alphabet.
Generator with controllability attributes.
void SetControllable(Idx index)
Mark event controllable (by index)
void DWrite(const Type *pContext=0) const
Write configuration data to console, debugging format.
Definition: cfl_types.cpp:225
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
void Write(const Type *pContext=0) const
Write configuration data to console.
Definition: cfl_types.cpp:139
Base class of all FAUDES generators.
void Name(const std::string &rName)
Set the generator's name.
virtual void Version(const std::string &rVersion, vGenerator &rResGen) const
Create another version of this generator.
void Parallel(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Parallel composition.
void InvProject(Generator &rGen, const EventSet &rProjectAlphabet)
Inverse projection.
void SupConNB(const Generator &rPlantGen, const EventSet &rCAlph, const Generator &rSpecGen, Generator &rResGen)
Nonblocking Supremal Controllable Sublanguage.
Definition: syn_supcon.cpp:757
Includes all libFAUDES headers, incl plugings
libFAUDES resides within the namespace faudes.
int main()

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