hyb_6_robotex.cpp
Go to the documentation of this file.
1 /** @file hyb_6_robotex.cpp
2 
3 Tutorial, hybrid systems plugin.
4 This tutorial sets up the patrol robot example and synthesises
5 a simple controller. It is used in a WODES and in a JDEDS
6 submission.
7 
8 @ingroup Tutorials
9 
10 @include hyb_6_robotex.cpp
11 
12 */
13 
14 #include "libfaudes.h"
15 #include "hyb_compute.h"
16 
17 // make the faudes namespace available to our program
18 using namespace faudes;
19 
20 
21 
22 /* generate plant model: robot on a grid */
23 /* option: use relative y-symbols (as opposed to absolute) */
24 // #define RELY
25 void robot(int szi, int szj, int mesh, int overlap, int disturbance, LinearHybridAutomaton& harobot, EventSet& uevents) {
26  // have input events (comment in/out to configure)
27  uevents.Clear();
28  uevents.Insert("u_north");
29  uevents.Insert("u_east");
30  uevents.Insert("u_south");
31  uevents.Insert("u_west");
32  //uevents.Insert("u_northeast");
33  //uevents.Insert("u_southeast");
34  //uevents.Insert("u_southwest");
35  //uevents.Insert("u_northwest");
36  harobot.InsEvents(uevents);
37  // support matrix A for 2 dim box
38  Matrix A42;
39  A42.Zero(4,2);
40  A42.At(0,0,-1);
41  A42.At(1,0, 1);
42  A42.At(2,1,-1);
43  A42.At(3,1, 1);
44  // generate bloated invariants per cell
45  std::vector< Polyhedron > Inv;
46  Inv.resize(szi*szj);
47  for(int i=0; i< szi; ++i) {
48  for(int j=0; j< szj; ++j) {
49  std::stringstream name;
50  name << "Inv_" << j+1 << "_" << i+1;
51  Vector Bij;
52  Bij.Zero(4);
53  Bij.At(0, -1* (mesh*j - 2*overlap));
54  Bij.At(1, (mesh*(j+1) + 2*overlap));
55  Bij.At(2, -1* (mesh*i - 2*overlap));
56  Bij.At(3, (mesh*(i+1) + 2*overlap));
57  Polyhedron Invij;
58  Invij.AB(A42,Bij);
59  Invij.Name(name.str());
60  Inv[i*szj+j]=Invij;
61  }
62  }
63  // generate the all-invariant aka continuous state set
64  Vector BAll;
65  BAll.Zero(4);
66  BAll.At(0, -1* (mesh*0 - 2*overlap));
67  BAll.At(1, (mesh*szj + 2*overlap));
68  BAll.At(2, -1* (mesh*0 - 2*overlap));
69  BAll.At(3, (mesh*szi + 2*overlap));
70  Polyhedron InvAll;
71  InvAll.AB(A42,BAll);
72  // generate right hand sides
73  std::vector< Polyhedron > Rate;
74  std::vector< std::string > Direction;
75  EventSet::Iterator uit=uevents.Begin();
76  EventSet::Iterator uit_end=uevents.End();
77  for(;uit!=uit_end;++uit) {
78  Vector F;
79  F.Zero(2);
80  if(uevents.SymbolicName(*uit)=="u_north") {
81  Direction.push_back("n");
82  F.At(0,0);
83  F.At(1,mesh);
84  }
85  if(uevents.SymbolicName(*uit)=="u_northeast") {
86  Direction.push_back("ne");
87  F.At(0,mesh);
88  F.At(1,mesh);
89  }
90  if(uevents.SymbolicName(*uit)=="u_east") {
91  Direction.push_back("e");
92  F.At(0,mesh);
93  F.At(1,0);
94  }
95  if(uevents.SymbolicName(*uit)=="u_southeast") {
96  Direction.push_back("se");
97  F.At(0,mesh);
98  F.At(1,-mesh);
99  }
100  if(uevents.SymbolicName(*uit)=="u_south") {
101  Direction.push_back("s");
102  F.At(0,0);
103  F.At(1,-mesh);
104  }
105  if(uevents.SymbolicName(*uit)=="u_southwest") {
106  Direction.push_back("sw");
107  F.At(0,-mesh);
108  F.At(1,-mesh);
109  }
110  if(uevents.SymbolicName(*uit)=="u_west") {
111  Direction.push_back("w");
112  F.At(0,-mesh);
113  F.At(1,0);
114  }
115  if(uevents.SymbolicName(*uit)=="u_northwest") {
116  Direction.push_back("nw");
117  F.At(0,-mesh);
118  F.At(1,mesh);
119  }
120  Vector Bd;
121  Bd.Zero(4);
122  Bd.At(0, -1* (F.At(0) - disturbance));
123  Bd.At(1, (F.At(0) + disturbance));
124  Bd.At(2, -1* (F.At(1) - disturbance));
125  Bd.At(3, (F.At(1) + disturbance));
126  Polyhedron Rated;
127  Rated.Name(Direction.back());
128  Rated.AB(A42,Bd);
129  Rate.push_back(Rated);
130  }
131  // generate the non-rate
132  Vector BNone;
133  BNone.Zero(4);
134  BNone.At(0, -1* 1 );
135  BNone.At(1, -1 );
136  BNone.At(2, -1* (1));
137  BNone.At(3, -1);
138  Polyhedron RateNone;
139  RateNone.AB(A42,BNone);
140  // set continuous state set and initial constraint
141  harobot.StateSpace(InvAll);
142  // set locations q(j,i,d)
143  for(int j=0; j< szj; ++j) {
144  for(int i=0; i< szi; ++i) {
145  for(int d=0; d<Direction.size(); ++d) {
146  std::stringstream name;
147  name << "q_" << j+1 << "_" << i+1 << "_" << Direction.at(d);
148  Idx q = harobot.InsState(name.str());
149  // rate by d
150  harobot.Rate(q,Rate.at(d));
151  // invariant by (j,i)
152  harobot.Invariant(q,Inv.at(i*szj + j));
153  }
154  }
155  }
156  // set locations q(j,i,?)
157  for(int j=0; j< szj; ++j) {
158  for(int i=0; i< szi; ++i) {
159  std::stringstream name;
160  name << "q_" << j+1 << "_" << i+1 << "_?";
161  Idx q = harobot.InsState(name.str());
162  // no-rate
163  harobot.Rate(q,RateNone);
164  // invariant by (j,i)
165  harobot.Invariant(q,Inv.at(i*szj + j));
166  // record initialstate (right upper)
167  /*
168  if((j+1==szj) && (i+1==szi)) {
169  harobot.InsInitState(q);
170  harobot.InitialConstraint(q,Inv.at(i*szj + j));
171  }
172  */
173  }
174  }
175  // set transitions from q(j,i,?)
176  for(int j=0; j< szj; ++j) {
177  for(int i=0; i< szi; ++i) {
178  std::stringstream name1;
179  name1 << "q_" << j+1 << "_" << i+1 << "_?";
180  Idx q1 = harobot.StateIndex(name1.str());
181  Idx q2,ev;
182  std::stringstream name2;
183  // north
184  name2 << "q_" << j+1 << "_" << i+1 << "_n";
185  q2 = harobot.StateIndex(name2.str());
186  ev=harobot.EventIndex("u_north");
187  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
188  // northeast
189  name2.str("");
190  name2 << "q_" << j+1 << "_" << i+1 << "_ne";
191  q2 = harobot.StateIndex(name2.str());
192  ev=harobot.EventIndex("u_northeast");
193  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
194  // east
195  name2.str("");
196  name2 << "q_" << j+1 << "_" << i+1 << "_e";
197  q2 = harobot.StateIndex(name2.str());
198  ev=harobot.EventIndex("u_east");
199  if(ev) harobot.SetTransition(q1,ev,q2);
200  // southeast
201  name2.str("");
202  name2 << "q_" << j+1 << "_" << i+1 << "_s";
203  q2 = harobot.StateIndex(name2.str());
204  ev=harobot.EventIndex("u_southeast");
205  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
206  // south
207  name2.str("");
208  name2 << "q_" << j+1 << "_" << i+1 << "_s";
209  q2 = harobot.StateIndex(name2.str());
210  ev=harobot.EventIndex("u_south");
211  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
212  // southwest
213  name2.str("");
214  name2 << "q_" << j+1 << "_" << i+1 << "_sw";
215  q2 = harobot.StateIndex(name2.str());
216  ev=harobot.EventIndex("u_southwest");
217  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
218  // west
219  name2.str("");
220  name2 << "q_" << j+1 << "_" << i+1 << "_w";
221  q2 = harobot.StateIndex(name2.str());
222  ev=harobot.EventIndex("u_west");
223  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
224  // northwest
225  name2.str("");
226  name2 << "q_" << j+1 << "_" << i+1 << "_nw";
227  q2 = harobot.StateIndex(name2.str());
228  ev=harobot.EventIndex("u_northwest");
229  if(harobot.ExistsEvent(ev)) harobot.SetTransition(q1,ev,q2);
230  }
231  }
232 #ifndef RELY
233  // have y-events
234  for(int j=0; j< szj; ++j) {
235  for(int i=0; i< szi; ++i) {
236  std::stringstream nameev;
237  if((j+1==szj) && (i+1 ==szi))
238  nameev << "y_A";
239  else if((j+1==1) && (i+1 ==1))
240  nameev << "y_B";
241  else
242  nameev << "y_" << j+1 << "_" << i+1;
243  harobot.InsEvent(nameev.str());
244  }
245  }
246 #else
247  // have y-events
248  harobot.InsEvent("y_n");
249  harobot.InsEvent("y_e");
250  harobot.InsEvent("y_s");
251  harobot.InsEvent("y_w");
252  harobot.InsEvent("y_A");
253  harobot.InsEvent("y_B");
254 #endif
255  // set transitions from q(j,i,!)
256  for(int j=0; j< szj; ++j) {
257  for(int i=0; i< szi; ++i) {
258  for(int d=0; d<Direction.size(); ++d) {
259  std::stringstream name1;
260  name1 << "q_" << j+1 << "_" << i+1 << "_" << Direction.at(d);
261  Idx q1 = harobot.StateIndex(name1.str());
262  Idx q2,ev;
263  std::stringstream name2;
264  std::stringstream nameev;
265  Vector Bgrd;
266  Polyhedron Grd;
267  // north neighbour
268  name2.str("");
269  name2 << "q_" << j+1 << "_" << i+1+1 << "_?";
270  q2 = harobot.StateIndex(name2.str());
271  nameev.str("");
272 #ifndef RELY
273  nameev << "y_" << j+1 << "_" << i+1+1;
274 #else
275  nameev << "y_n";
276 #endif
277  if((j+1==1) && (i+1+1 ==1)) {
278  nameev.str("");
279  nameev << "y_B";
280  }
281  if((j+1==szj) && (i+1+1==szi)) {
282  nameev.str("");
283  nameev << "y_A";
284  }
285  ev = harobot.EventIndex(nameev.str());
286  if((q2!=0) && (ev!=0)) {
287  // transition
288  harobot.SetTransition(q1,ev,q2);
289  // north guard
290  Bgrd.Zero(4);
291  Bgrd.At(0, -1* (mesh*j - 2*overlap));
292  Bgrd.At(1, (mesh*(j+1) + 2*overlap));
293  Bgrd.At(2, -1* (mesh*(i+1) + 1*overlap));
294  Bgrd.At(3, (mesh*(i+1) + 2*overlap));
295  Grd.AB(A42,Bgrd);
296  harobot.Guard(Transition(q1,ev,q2),Grd);
297  }
298  // east neighbour
299  name2.str("");
300  name2 << "q_" << j+1+1 << "_" << i+1 << "_?";
301  q2 = harobot.StateIndex(name2.str());
302  nameev.str("");
303 #ifndef RELY
304  nameev << "y_" << j+1+1 << "_" << i+1;
305 #else
306  nameev << "y_e";
307 #endif
308  if((j+1+1==1) && (i+1==1)) {
309  nameev.str("");
310  nameev << "y_B";
311  }
312  if((j+1+1==szj) && (i+1==szi)) {
313  nameev.str("");
314  nameev << "y_A";
315  }
316  ev = harobot.EventIndex(nameev.str());
317  if((q2!=0) && (ev!=0)) {
318  // transition
319  harobot.SetTransition(q1,ev,q2);
320  // east guard
321  Bgrd.Zero(4);
322  Bgrd.At(0, -1* (mesh*(j+1) + 1*overlap));
323  Bgrd.At(1, (mesh*(j+1) + 2*overlap));
324  Bgrd.At(2, -1* (mesh*(i) - 2*overlap));
325  Bgrd.At(3, (mesh*(i+1) + 2*overlap));
326  Grd.AB(A42,Bgrd);
327  harobot.Guard(Transition(q1,ev,q2),Grd);
328  }
329  // south neighbour
330  name2.str("");
331  name2 << "q_" << j+1 << "_" << i+1-1 << "_?";
332  q2 = harobot.StateIndex(name2.str());
333  nameev.str("");
334 #ifndef RELY
335  nameev << "y_" << j+1 << "_" << i+1-1;
336 #else
337  nameev << "y_s";
338 #endif
339  if((j+1==1) && (i+1-1 ==1)) {
340  nameev.str("");
341  nameev << "y_B";
342  }
343  if((j+1==szj) && (i+1-1==szi)) {
344  nameev.str("");
345  nameev << "y_A";
346  }
347  ev = harobot.EventIndex(nameev.str());
348  if((q2!=0) && (ev!=0)) {
349  // transition
350  harobot.SetTransition(q1,ev,q2);
351  // south guard
352  Bgrd.Zero(4);
353  Bgrd.At(0, -1* (mesh*j - 2*overlap));
354  Bgrd.At(1, (mesh*(j+1) + 2*overlap));
355  Bgrd.At(2, -1* (mesh*(i) - 2*overlap));
356  Bgrd.At(3, (mesh*(i) - 1*overlap));
357  Grd.AB(A42,Bgrd);
358  harobot.Guard(Transition(q1,ev,q2),Grd);
359  }
360  // west neighbour
361  name2.str("");
362  name2 << "q_" << j+1-1 << "_" << i+1 << "_?";
363  q2 = harobot.StateIndex(name2.str());
364  nameev.str("");
365 #ifndef RELY
366  nameev << "y_" << j+1-1 << "_" << i+1;
367 #else
368  nameev << "y_w";
369 #endif
370  if((j+1-1==1) && (i+1 ==1)) {
371  nameev.str("");
372  nameev << "y_B";
373  }
374  if((j+1-1==szj) && (i+1==szi)) {
375  nameev.str("");
376  nameev << "y_A";
377  }
378  ev = harobot.EventIndex(nameev.str());
379  if((q2!=0) && (ev!=0)) {
380  // transition
381  harobot.SetTransition(q1,ev,q2);
382  // west guard
383  Bgrd.Zero(4);
384  Bgrd.At(0, -1* (mesh*(j) - 2*overlap));
385  Bgrd.At(1, (mesh*(j) - 1*overlap));
386  Bgrd.At(2, -1* (mesh*(i) - 2*overlap));
387  Bgrd.At(3, (mesh*(i+1) + 2*overlap));
388  Grd.AB(A42,Bgrd);
389  harobot.Guard(Transition(q1,ev,q2),Grd);
390  }
391  }
392  }
393  }
394  // optional: unconstraint version
395  StateSet::Iterator sit= harobot.StatesBegin();
396  StateSet::Iterator sit_end= harobot.StatesEnd();
397  for(;sit!=sit_end;++sit) {
398  harobot.InsInitState(*sit);
399  harobot.InitialConstraint(*sit,harobot.Invariant(*sit));
400  }
401 }
402 
403 
404 /* generate plant model: time invariant marine vehicle within a rectangualr area */
405 void marine(int width, int height, int overlap, int velocity, int disturbance, LinearHybridAutomaton& hamarine, EventSet& uevents) {
406  // have input events (comment in/out to configure)
407  uevents.Clear();
408  uevents.Insert("u_northeast");
409  uevents.Insert("u_southeast");
410  uevents.Insert("u_southwest");
411  uevents.Insert("u_northwest");
412  hamarine.InsEvents(uevents);
413  // support matrix A for 2 dim box
414  Matrix A42;
415  A42.Zero(4,2);
416  A42.At(0,0,-1);
417  A42.At(1,0, 1);
418  A42.At(2,1,-1);
419  A42.At(3,1, 1);
420  // generate the all-invariant aka continuous state set
421  Vector BAll;
422  BAll.Zero(4);
423  BAll.At(0, -1* 0 );
424  BAll.At(1, width );
425  BAll.At(2, -1* 0 );
426  BAll.At(3, height);
427  Polyhedron InvAll;
428  InvAll.AB(A42,BAll);
429  // generate right hand sides
430  std::vector< Polyhedron > Rate;
431  std::vector< std::string > Direction;
432  EventSet::Iterator uit=uevents.Begin();
433  EventSet::Iterator uit_end=uevents.End();
434  for(;uit!=uit_end;++uit) {
435  Vector F;
436  F.Zero(2);
437  if(uevents.SymbolicName(*uit)=="u_north") {
438  Direction.push_back("n");
439  F.At(0,0);
440  F.At(1,velocity);
441  }
442  if(uevents.SymbolicName(*uit)=="u_northeast") {
443  Direction.push_back("ne");
444  F.At(0,velocity);
445  F.At(1,velocity);
446  }
447  if(uevents.SymbolicName(*uit)=="u_east") {
448  Direction.push_back("e");
449  F.At(0,velocity);
450  F.At(1,0);
451  }
452  if(uevents.SymbolicName(*uit)=="u_southeast") {
453  Direction.push_back("se");
454  F.At(0,velocity);
455  F.At(1,-velocity);
456  }
457  if(uevents.SymbolicName(*uit)=="u_south") {
458  Direction.push_back("s");
459  F.At(0,0);
460  F.At(1,-velocity);
461  }
462  if(uevents.SymbolicName(*uit)=="u_southwest") {
463  Direction.push_back("sw");
464  F.At(0,-velocity);
465  F.At(1,-velocity);
466  }
467  if(uevents.SymbolicName(*uit)=="u_west") {
468  Direction.push_back("w");
469  F.At(0,-velocity);
470  F.At(1,0);
471  }
472  if(uevents.SymbolicName(*uit)=="u_northwest") {
473  Direction.push_back("nw");
474  F.At(0,-velocity);
475  F.At(1,velocity);
476  }
477  Vector Bd;
478  Bd.Zero(4);
479  Bd.At(0, -1* (F.At(0) - disturbance));
480  Bd.At(1, (F.At(0) + disturbance));
481  Bd.At(2, -1* (F.At(1) - disturbance));
482  Bd.At(3, (F.At(1) + disturbance));
483  Polyhedron Rated;
484  Rated.Name(Direction.back());
485  Rated.AB(A42,Bd);
486  Rate.push_back(Rated);
487  }
488  // generate the non-rate
489  Vector BNone;
490  BNone.Zero(4);
491  BNone.At(0, -1* 1 );
492  BNone.At(1, -1 );
493  BNone.At(2, -1* (1));
494  BNone.At(3, -1);
495  Polyhedron RateNone;
496  RateNone.AB(A42,BNone);
497  // set continuous state set and initial constraint
498  hamarine.StateSpace(InvAll);
499  // set locations q(d)
500  for(int d=0; d<Direction.size(); ++d) {
501  std::stringstream name;
502  name << "q_" << Direction.at(d);
503  Idx q = hamarine.InsState(name.str());
504  // rate by d
505  hamarine.Rate(q,Rate.at(d));
506  // invariant by (j,i)
507  hamarine.Invariant(q,InvAll);
508  }
509  // set location q(?)
510  std::string nameqq="q_?";
511  Idx qq = hamarine.InsInitState(nameqq);
512  hamarine.Rate(qq,RateNone);
513  hamarine.Invariant(qq,InvAll);
514  // set transitions from q(?)
515  uit=uevents.Begin();
516  uit_end=uevents.End();
517  for(;uit!=uit_end;++uit) {
518  Idx ev=*uit;
519  Idx qn;
520  std::string nameqn;
521  if(uevents.SymbolicName(*uit)=="u_northeast")
522  nameqn="q_ne";
523  if(uevents.SymbolicName(*uit)=="u_northwest")
524  nameqn="q_nw";
525  if(uevents.SymbolicName(*uit)=="u_southwest")
526  nameqn="q_sw";
527  if(uevents.SymbolicName(*uit)=="u_southeast")
528  nameqn="q_se";
529  if(nameqn=="")
530  std::cout << "Setting up model: INTERNAL ERRROR A\n";
531  qn=hamarine.StateIndex(nameqn);
532  hamarine.SetTransition(qq,*uit,qn);
533  }
534  // have y-events
535  hamarine.InsEvent("y_n");
536  hamarine.InsEvent("y_e");
537  hamarine.InsEvent("y_s");
538  hamarine.InsEvent("y_w");
539  // set transitions from q(!)
540  for(int d=0; d<Direction.size(); ++d) {
541  std::string namen = "q_" + Direction.at(d);
542  Idx qn=hamarine.StateIndex(namen);
543  Vector Bgrd;
544  Polyhedron Grd;
545  Idx ev;
546  std::string nameev;
547  // north boundary
548  if((Direction.at(d)=="ne") || (Direction.at(d)=="nw")) {
549  nameev = "y_n";
550  ev = hamarine.EventIndex(nameev);
551  hamarine.SetTransition(qn,ev,qq);
552  // north guard
553  Bgrd.Zero(4);
554  Bgrd.At(0, -1* (0 ));
555  Bgrd.At(1, (width ));
556  Bgrd.At(2, -1* (height - overlap));
557  Bgrd.At(3, (height ));
558  Grd.AB(A42,Bgrd);
559  hamarine.Guard(Transition(qn,ev,qq),Grd);
560  }
561  // south boundary
562  if((Direction.at(d)=="se") || (Direction.at(d)=="sw")) {
563  nameev = "y_s";
564  ev = hamarine.EventIndex(nameev);
565  hamarine.SetTransition(qn,ev,qq);
566  // south guard
567  Bgrd.Zero(4);
568  Bgrd.At(0, -1* (0 ));
569  Bgrd.At(1, (width ));
570  Bgrd.At(2, -1* (0 ));
571  Bgrd.At(3, (overlap ));
572  Grd.AB(A42,Bgrd);
573  hamarine.Guard(Transition(qn,ev,qq),Grd);
574  }
575  // west boundary
576  if((Direction.at(d)=="nw") || (Direction.at(d)=="sw")) {
577  nameev = "y_w";
578  ev = hamarine.EventIndex(nameev);
579  hamarine.SetTransition(qn,ev,qq);
580  // west guard
581  Bgrd.Zero(4);
582  Bgrd.At(0, -1* (0 ));
583  Bgrd.At(1, (overlap ));
584  Bgrd.At(2, -1* (0 ));
585  Bgrd.At(3, (height ));
586  Grd.AB(A42,Bgrd);
587  hamarine.Guard(Transition(qn,ev,qq),Grd);
588  }
589  // east boundary
590  if((Direction.at(d)=="ne") || (Direction.at(d)=="se")) {
591  nameev = "y_e";
592  ev = hamarine.EventIndex(nameev);
593  hamarine.SetTransition(qn,ev,qq);
594  // east guard
595  Bgrd.Zero(4);
596  Bgrd.At(0, -1* (width-overlap ));
597  Bgrd.At(1, (width ));
598  Bgrd.At(2, -1* (0 ));
599  Bgrd.At(3, (height ));
600  Grd.AB(A42,Bgrd);
601  hamarine.Guard(Transition(qn,ev,qq),Grd);
602  }
603  }
604  // optional: still unconstraint, but must start with u-event
605  hamarine.InitialConstraint(qq,InvAll);
606 }
607 
608 /* excute interactively */
609 int execute(LinearHybridAutomaton& plant, HybridStateSet& cstates) {
610 
611  // compute reachable states per successor event
612  std::map< Idx, HybridStateSet* > sstatespe;
613  LhaReach(plant,cstates,sstatespe);
614 
615  // show current state
616  std::cout << "################################\n";
617  std::cout << "# current state set \n";
618  cstates.DWrite(plant);
619  std::cout << "################################\n";
620 
621  // show mode transitions
622  std::cout << "################################\n";
623  std::cout << "# mode transitions \n";
624  IndexSet::Iterator qit=cstates.LocationsBegin();
625  IndexSet::Iterator qit_end=cstates.LocationsEnd();
626  for(;qit!=qit_end;++qit){
627  TransSet::Iterator tit=plant.TransRelBegin(*qit);
628  TransSet::Iterator tit_end=plant.TransRelEnd(*qit);
629  for(;tit!=tit_end;++tit)
630  std::cout << plant.TStr(*tit) << "\n";
631  }
632  std::cout << "################################\n";
633 
634 
635  // show next events
636  std::cout << "################################\n";
637  std::cout << "# successor events \n";
638  std::map< Idx, HybridStateSet* >::iterator sit=sstatespe.begin();
639  std::map< Idx, HybridStateSet* >::iterator sit_end=sstatespe.end();
640  EventSet enabled;
641  for(;sit!=sit_end;++sit) {
642  enabled.Insert(sit->first);
643  std::cout << plant.EStr(sit->first) << " ";
644  //std::cout << "\n# successor states for " << plant.EStr(sit->first) << "\n";
645  //sit->second->DWrite(plant);
646  }
647  std::cout << "\n################################\n";
648 
649  // interactive loop until accept
650  while(true) {
651 
652  // choose event
653  Idx ev;
654  while(true) {
655  std::cout << "choose event (or 'x' for exit): ";
656  std::string choice;
657  std::cin>>choice;
658  if(choice=="x") return 0;
659  ev=ToIdx(choice);
660  if(enabled.Exists(ev)) break;
661  ev=plant.EventIndex(choice);
662  if(enabled.Exists(ev)) break;
663  }
664  sit=sstatespe.find(ev);
665 
666  // dump successor states
667  std::cout << "################################\n";
668  std::cout << "# successor states for " << plant.EStr(sit->first) << "\n";
669  sit->second->DWrite(plant);
670  std::cout << "################################\n";
671 
672  // accept choice
673  std::cout << "accept ('n' for no, other for yes): ";
674  std::string choice;
675  std::cin>>choice;
676  if(choice!="n") break;
677 
678  } // end interactive
679 
680  // update states
681  cstates.Assign(*sit->second);
682 
683  // report event
684  return sit->first;
685 }
686 
687 
688 /** Run the tutorial: time variant robot, target control */
689 int robot2017() {
690 
691  /** generate plant */
692  LinearHybridAutomaton lioha;
693  EventSet uevents;
694  robot(3 /* rows */, 5 /*cols*/ , 10 /* mesh */, 1 /* overlap */, 1 /* disturbance */, lioha, uevents);
695 
696  // report to console
697  /*
698  std::cout << "################################\n";
699  std::cout << "# linear hybrid automaton: \n";
700  lioha.Write();
701  std::cout << "################################\n";
702  std::cout << "# Valid() returns " << lioha.Valid() << "\n";
703  std::cout << "################################\n";
704  */
705 
706  // get initial state
707  HybridStateSet istates;
708  StateSet::Iterator qit=lioha.InitStatesBegin();
709  StateSet::Iterator qit_end=lioha.InitStatesEnd();
710  for(;qit!=qit_end;++qit){
711  Polyhedron* poly = new Polyhedron(lioha.InitialConstraint(*qit));
712  PolyIntersection(lioha.StateSpace(),*poly);
713  PolyFinalise(*poly);
714  istates.Insert(*qit,poly);
715  }
716 
717  /*
718  std::cout << "################################\n";
719  std::cout << "# dumping initial states\n";
720  istates.DWrite(lioha);
721  std::cout << "################################\n";
722  */
723 
724  // run interactively for manual inspection
725  HybridStateSet cstates;
726  cstates.Assign(istates);
727  while(true) {
728  Idx ev=execute(lioha,cstates);
729  if(ev==0) break;
730  }
731 
732 
733  // prepare abstraction
734  int theL=2;
735  LhaCompatibleStates* comp;
736  Experiment* exp;
737 
738  // do l-complete abstraction from scratch (time variant)
739  std::cout << "################################\n";
740  std::cout << "# compute l-complete approximation, time variant \n";
741  std::cout << "################################\n";
742  comp = new LhaCompatibleStates(lioha);
743  comp->InitialiseConstraint();
744  exp = new Experiment(lioha.Alphabet());
745  exp->InitialStates(comp);
746  LbdAbstraction tvabs;
747  tvabs.Experiment(exp);
748  tvabs.RefineUniformly(theL);
749 
750  // Do l-complete abstraction from scratch (time invariant)
751  std::cout << "################################\n";
752  std::cout << "# compute l-complete approximation, time invariant \n";
753  std::cout << "################################\n";
754  comp = new LhaCompatibleStates(lioha);
755  comp->InitialiseFull();
756  exp = new Experiment(lioha.Alphabet());
757  exp->InitialStates(comp);
758  LbdAbstraction tivabs;
759  tivabs.Experiment(exp);
760  tivabs.RefineUniformly(theL);
761 
762  // loop refine
763  while(true) {
764 
765  // compose both for finest result
766  std::cout << "################################\n";
767  std::cout << "# compose abstraction \n";
768  std::cout << "################################\n";
769  tvabs.Experiment().SWrite();
770  tivabs.Experiment().SWrite();
771  tvabs.TvAbstraction().SWrite();
772  tivabs.TivAbstraction().SWrite();
773  Generator abst;
774  abst.StateNamesEnabled(false);
775  ProductCompositionMap cmap_tv_tiv;
776  aProduct(tvabs.TvAbstraction(),tivabs.TivAbstraction(),cmap_tv_tiv,abst);
777  //abst=tivabs.TivAbstraction();
778  MarkAllStates(abst);
779 
780 
781  // report statistics
782  abst.SWrite();
783  //abst.GraphWrite("tmp_lv4.png");
784 
785  std::cout << "################################\n";
786  std::cout << "# target control synthesis \n";
787  std::cout << "# ctrl evs " << uevents.ToString() << "\n";
788  std::cout << "################################\n";
789 
790  // target specification by y
791  Generator spec;
792  spec.InjectAlphabet(lioha.Alphabet());
793  Idx s0=spec.InsInitState();
794  Idx st=spec.InsMarkedState();
795  spec.SetTransition(s0,spec.EventIndex("y_target"),st);
796  spec.SetTransition(st,spec.EventIndex("y_target"),st);
797  EventSet sfloop=lioha.Alphabet();
798  sfloop.Erase("y_target");
799  //sfloop.Erase("u_east");
800  SelfLoop(spec,sfloop);
801 
802  /*
803  // target specification by xtarget
804  Generator spec=abst;
805  spec.ClearMarkedStates();
806  StateSet::Iterator csit=abst.StatesBegin();
807  StateSet::Iterator csit_end=abst.StatesEnd();
808  for(;csit!=csit_end;++csit) {
809  Idx qabstv = cmap_tv_tiv.Arg1State(*csit);
810  bool ok_tv=true;
811  const LhaCompatibleStates* pHstates = dynamic_cast<const LhaCompatibleStates*>(tvabs.Experiment().States(qabstv));
812  if(!pHstates)
813  throw Exception("hyb_6_robotex(..)", "incompatible cstates type A", 90);
814  IndexSet::Iterator lit = pHstates->States()->LocationsBegin();
815  IndexSet::Iterator lit_end = pHstates->States()->LocationsEnd();
816  for(;lit!=lit_end;++lit) {
817  HybridStateSet::Iterator sit = pHstates->States()->StatesBegin(*lit);
818  HybridStateSet::Iterator sit_end = pHstates->States()->StatesEnd(*lit);
819  for(;sit!=sit_end;++sit)
820  if(!PolyInclusion(**sit,xtarget)) { ok_tv=false; break;}
821  }
822  Idx qabstiv = cmap_tv_tiv.Arg2State(*csit);
823  bool ok_tiv=true;
824  pHstates = dynamic_cast<const LhaCompatibleStates*>(tivabs.Experiment().States(qabstiv));
825  if(!pHstates)
826  throw Exception("hyb_6_robotex(..)", "incompatible cstates type B", 90);
827  lit = pHstates->States()->LocationsBegin();
828  lit_end = pHstates->States()->LocationsEnd();
829  for(;lit!=lit_end;++lit) {
830  HybridStateSet::Iterator sit = pHstates->States()->StatesBegin(*lit);
831  HybridStateSet::Iterator sit_end = pHstates->States()->StatesEnd(*lit);
832  for(;sit!=sit_end;++sit)
833  if(!PolyInclusion(**sit,xtarget)) { ok_tiv=false; break;}
834  }
835  if(ok_tiv || ok_tv) {
836  spec.InsMarkedState(*csit);
837  }
838  }
839  std::cout << "# found #" << spec.MarkedStates().Size() << " good states\n";
840  */
841 
842  // target control: reach marked state
843  Generator loop;
844  ProductCompositionMap cmap_abst_spec;
845  aProduct(abst,spec,cmap_abst_spec,loop);
846  StateSet good=loop.MarkedStates();
847  while(true) {
848  int gsz=good.Size();
849  std::cout << "target control: #" << gsz << " / #" << loop.Size() << "\n";
850  StateSet::Iterator sit=loop.StatesBegin();
851  StateSet::Iterator sit_end=loop.StatesEnd();
852  for(;sit!=sit_end;++sit) {
853  if(good.Exists(*sit)) continue;
854  bool ok=false;
855  TransSet::Iterator tit=loop.TransRelBegin(*sit);
856  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
857  for(;tit!=tit_end;++tit) {
858  if(good.Exists(tit->X2)) {ok=true; continue;}
859  if(uevents.Exists(tit->Ev)) continue;
860  ok=false;
861  break;
862  }
863  if(ok) good.Insert(*sit);
864  }
865  if(good.Size()==gsz) break;
866  }
867  std::cout << "target control: #" << good.Size() << " / #" << loop.Size() << "\n";
868  bool success=good.Exists(loop.InitState());
869  if(success)
870  std::cout << "target control: success (init state #" << loop.InitState() << " found to be good)\n";
871  else
872  std::cout << "target control: FAIL\n";
873  if(success) {
874  return 0;
875  }
876 
877  // diagnose failure
878  StateSet tvleaves;
879  StateSet tivleaves;
880  StateSet::Iterator sit=loop.StatesBegin();
881  StateSet::Iterator sit_end=loop.StatesEnd();
882  for(;sit!=sit_end;++sit) {
883  // ok done
884  if(good.Exists(*sit)) continue;
885  // sort states
886  Idx qabs = cmap_abst_spec.Arg1State(*sit);
887  Idx qtvabs = cmap_tv_tiv.Arg1State(qabs);
888  Idx qtivabs = cmap_tv_tiv.Arg2State(qabs);
889  // allways refine
890  if(tivabs.Experiment().IsLeave(qtivabs)) tivleaves.Insert(qtivabs);
891  if(tvabs.Experiment().IsLeave(qtvabs)) tvleaves.Insert(qtvabs);
892  TransSet::Iterator tit=loop.TransRelBegin(*sit);
893  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
894  for(;tit!=tit_end;++tit) {
895  if(good.Exists(tit->X2)) break;
896  TransSet::Iterator tit2=loop.TransRelBegin(tit->X2);
897  TransSet::Iterator tit2_end=loop.TransRelEnd(tit->X2);
898  for(;tit2!=tit2_end;++tit2) {
899  if(good.Exists(tit2->X2)) break;
900  }
901  if(tit2!=tit2_end) break;
902  }
903  if(tit==tit_end) continue;
904  // refine on on chance for success
905  if(tivabs.Experiment().IsLeave(qtivabs)) tivleaves.Insert(qtivabs);
906  if(tvabs.Experiment().IsLeave(qtvabs)) tvleaves.Insert(qtvabs);
907  }
908  std::cout << "################################\n";
909  std::cout << "# diagnosis\n";
910  std::cout << "# tv-leaves to refine #" << tvleaves.Size() << "/" << tvabs.Experiment().Leaves().Size() << "\n";
911  std::cout << "# tiv-leaves to refine #" << tivleaves.Size() << "/" << tivabs.Experiment().Leaves().Size() << "\n";
912  std::cout << "################################\n";
913 
914 
915  // do refine
916  std::cout << "################################\n";
917  std::cout << "# refine\n";
918  std::cout << "################################\n";
919  sit=tvleaves.Begin();
920  sit_end=tvleaves.End();
921  for(;sit!=sit_end;++sit) {
922  tvabs.RefineAt(*sit);
923  }
924  sit=tivleaves.Begin();
925  sit_end=tivleaves.End();
926  for(;sit!=sit_end;++sit) {
927  tivabs.RefineAt(*sit);
928  }
929 
930  // loop refine/synthesis
931  }
932 
933 
934  // done
935  return 0;
936 }
937 
938 
939 /** Run the tutorial: time invariant robot */
940 int robot2018ti() {
941 
942  /** generate plant */
943  LinearHybridAutomaton lioha;
944  EventSet uevents;
945  robot(3 /* rows */, 5 /*cols*/ , 10 /* mesh */, 1 /* overlap */, 1 /* disturbance */, lioha, uevents);
946 
947  // report to console
948  /*
949  std::cout << "################################\n";
950  std::cout << "# linear hybrid automaton: \n";
951  lioha.Write();
952  std::cout << "################################\n";
953  std::cout << "# Valid() returns " << lioha.Valid() << "\n";
954  std::cout << "################################\n";
955  */
956 
957  // get initial state
958  HybridStateSet istates;
959  StateSet::Iterator qit=lioha.InitStatesBegin();
960  StateSet::Iterator qit_end=lioha.InitStatesEnd();
961  for(;qit!=qit_end;++qit){
962  Polyhedron* poly = new Polyhedron(lioha.InitialConstraint(*qit));
963  PolyIntersection(lioha.StateSpace(),*poly);
964  PolyFinalise(*poly);
965  istates.Insert(*qit,poly);
966  }
967 
968  /*
969  std::cout << "################################\n";
970  std::cout << "# dumping initial states\n";
971  istates.DWrite(lioha);
972  std::cout << "################################\n";
973  */
974 
975  // run interactively for manual inspection
976  HybridStateSet cstates;
977  cstates.Assign(istates);
978  while(true) {
979  Idx ev=execute(lioha,cstates);
980  if(ev==0) break;
981  }
982 
983 
984  // prepare abstraction
985  int theL=2;
986  LhaCompatibleStates* comp;
987  Experiment* exp;
988 
989  // Do l-complete abstraction from scratch (time invariant)
990  std::cout << "################################\n";
991  std::cout << "# compute l-complete approximation, time invariant \n";
992  std::cout << "################################\n";
993  comp = new LhaCompatibleStates(lioha);
994  comp->InitialiseFull();
995  exp = new Experiment(lioha.Alphabet());
996  exp->InitialStates(comp);
997  LbdAbstraction tivabs;
998  tivabs.Experiment(exp);
999  tivabs.RefineUniformly(theL);
1000 
1001  // loop refine
1002  while(true) {
1003 
1004  // copy abstraction
1005  Generator abst=tivabs.TivAbstraction();
1006  abst.StateNamesEnabled(false);
1007  MarkAllStates(abst);
1008  abst.Name("overall abstraction");
1009 
1010  // report statistics
1011  tivabs.Experiment().SWrite();
1012  abst.Write("tmp_abs2.gen");
1013 
1014  std::cout << "################################\n";
1015  std::cout << "# cycle control synthesis \n";
1016  std::cout << "# ctrl evs " << uevents.ToString() << "\n";
1017  std::cout << "################################\n";
1018 
1019  // A/B target specification by y
1020  Generator spec;
1021  spec.InjectAlphabet(lioha.Alphabet());
1022  Idx sga=spec.InsInitState();
1023  Idx sgb=spec.InsState();
1024  Idx ssa=spec.InsMarkedState();
1025  Idx ssb=spec.InsMarkedState();
1026  spec.SetTransition(sga,spec.EventIndex("y_A"),ssa);
1027  spec.SetTransition(sga,spec.EventIndex("y_B"),sga);
1028  spec.SetTransition(ssa,spec.EventIndex("y_A"),sgb);
1029  spec.SetTransition(ssa,spec.EventIndex("y_B"),ssb);
1030  spec.SetTransition(sgb,spec.EventIndex("y_B"),ssb);
1031  spec.SetTransition(sgb,spec.EventIndex("y_A"),sgb);
1032  spec.SetTransition(ssb,spec.EventIndex("y_B"),sga);
1033  spec.SetTransition(ssb,spec.EventIndex("y_A"),ssa);
1034  EventSet other=lioha.Alphabet();
1035  other.Erase("y_A");
1036  other.Erase("y_B");
1037  EventSet::Iterator eit=other.Begin();
1038  for(;eit!=other.End();++eit) {
1039  spec.SetTransition(sga,*eit,sga);
1040  spec.SetTransition(ssa,*eit,sgb);
1041  spec.SetTransition(sgb,*eit,sgb);
1042  spec.SetTransition(ssb,*eit,sga);
1043  }
1044  spec.GraphWrite("tmp_spec.png");
1045 
1046  // target control: reach marked state inf often
1047  Generator loop;
1048  ProductCompositionMap cmap_abst_spec;
1049  aProduct(abst,spec,cmap_abst_spec,loop);
1050  StateSet constraint = loop.States();
1051  StateSet winning;
1052 
1053  while(true) {
1054  StateSet target = loop.MarkedStates();
1055  target.RestrictSet(constraint);
1056  int csz=constraint.Size();
1057  int tsz=target.Size();
1058  std::cout << "target control: constraint #" << csz << " target #" << tsz << "\n";
1059  winning.Clear();
1060 
1061  while(true) {
1062  int wsz=winning.Size();
1063  std::cout << "target control: #" << wsz << " / #" << loop.Size() << "\n";
1064  StateSet ctrlreach;
1065  StateSet::Iterator sit=loop.StatesBegin();
1066  StateSet::Iterator sit_end=loop.StatesEnd();
1067  for(;sit!=sit_end;++sit) {
1068  if(winning.Exists(*sit)) continue;
1069  bool ok=false;
1070  TransSet::Iterator tit=loop.TransRelBegin(*sit);
1071  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
1072  for(;tit!=tit_end;++tit) {
1073  if(winning.Exists(tit->X2)) {ok=true; continue;}
1074  if(target.Exists(tit->X2)) {ok=true; continue;}
1075  if(uevents.Exists(tit->Ev)) continue;
1076  ok=false;
1077  break;
1078  }
1079  if(ok) ctrlreach.Insert(*sit);
1080  }
1081  if(ctrlreach <= winning) break;
1082  winning.InsertSet(ctrlreach);
1083  }
1084 
1085  constraint.RestrictSet(winning);
1086  if(csz==constraint.Size()) break;
1087  }
1088 
1089  std::cout << "target control: #" << winning.Size() << " / #" << loop.Size() << "\n";
1090  bool success=winning.Exists(loop.InitState());
1091  if(success)
1092  std::cout << "target control: success (init state #" << loop.InitState() << " found to be winning)\n";
1093  else
1094  std::cout << "target control: FAIL\n";
1095  if(success) {
1096  return 0;
1097  }
1098 
1099  // diagnose failure
1100  StateSet tvleaves;
1101  StateSet tivleaves;
1102  StateSet::Iterator sit=loop.StatesBegin();
1103  StateSet::Iterator sit_end=loop.StatesEnd();
1104  for(;sit!=sit_end;++sit) {
1105  // ok done
1106  if(winning.Exists(*sit)) continue;
1107  // sort states
1108  Idx qtivabs = cmap_abst_spec.Arg1State(*sit);
1109  // allways refine
1110  if(tivabs.Experiment().IsLeave(qtivabs)) tivleaves.Insert(qtivabs);
1111  // is there a chance to win?
1112  TransSet::Iterator tit=loop.TransRelBegin(*sit);
1113  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
1114  for(;tit!=tit_end;++tit) {
1115  if(winning.Exists(tit->X2)) break;
1116  TransSet::Iterator tit2=loop.TransRelBegin(tit->X2);
1117  TransSet::Iterator tit2_end=loop.TransRelEnd(tit->X2);
1118  for(;tit2!=tit2_end;++tit2) {
1119  if(winning.Exists(tit2->X2)) break;
1120  }
1121  if(tit2!=tit2_end) break;
1122  }
1123  if(tit==tit_end) continue;
1124  // refine on a chance for success
1125  if(tivabs.Experiment().IsLeave(qtivabs)) tivleaves.Insert(qtivabs);
1126  }
1127  std::cout << "################################\n";
1128  std::cout << "# diagnosis\n";
1129  std::cout << "# tiv-leaves to refine #" << tivleaves.Size() << "/" << tivabs.Experiment().Leaves().Size() << "\n";
1130  std::cout << "################################\n";
1131 
1132 
1133  // do refine
1134  std::cout << "################################\n";
1135  std::cout << "# refine\n";
1136  std::cout << "################################\n";
1137  sit=tivleaves.Begin();
1138  sit_end=tivleaves.End();
1139  for(;sit!=sit_end;++sit) {
1140  tivabs.RefineAt(*sit);
1141  }
1142 
1143  // loop refine/synthesis
1144  }
1145 
1146 
1147  // done
1148  return 0;
1149 }
1150 
1151 
1152 /** Run the tutorial: time invariant marine */
1153 int marine2018() {
1154 
1155  /** generate plant */
1156  LinearHybridAutomaton lioha;
1157  EventSet uevents;
1158  marine(30 /* width */, 10 /*height*/ , 1 /*overlap*/, 10 /*velo*/, 1 /* disturbance */, lioha, uevents);
1159  EventSet yevents = lioha.Alphabet();
1160  yevents.EraseSet(uevents);
1161 
1162  // report to console
1163  std::cout << "################################\n";
1164  std::cout << "# linear hybrid automaton: \n";
1165  lioha.Write();
1166  std::cout << "################################\n";
1167  std::cout << "# Valid() returns " << lioha.Valid() << "\n";
1168  std::cout << "################################\n";
1169 
1170  // get initial state
1171  HybridStateSet istates;
1172  StateSet::Iterator qit=lioha.InitStatesBegin();
1173  StateSet::Iterator qit_end=lioha.InitStatesEnd();
1174  for(;qit!=qit_end;++qit){
1175  Polyhedron* poly = new Polyhedron(lioha.InitialConstraint(*qit));
1176  PolyIntersection(lioha.StateSpace(),*poly);
1177  PolyFinalise(*poly);
1178  istates.Insert(*qit,poly);
1179  }
1180 
1181  // run interactively for manual inspection
1182  HybridStateSet cstates;
1183  cstates.Assign(istates);
1184  while(true) {
1185  Idx ev=execute(lioha,cstates);
1186  if(ev==0) break;
1187  }
1188 
1189  // prepare abstraction
1190  int theL=2;
1191  LhaCompatibleStates* comp;
1192  Experiment* exp;
1193 
1194  // Do l-complete abstraction from scratch (time invariant)
1195  std::cout << "################################\n";
1196  std::cout << "# compute l-complete approximation, time invariant \n";
1197  std::cout << "################################\n";
1198  comp = new LhaCompatibleStates(lioha);
1199  comp->InitialiseConstraint(); // still time invariant but start with u-event
1200  exp = new Experiment(lioha.Alphabet());
1201  exp->InitialStates(comp);
1202  LbdAbstraction tivabs;
1203  tivabs.Experiment(exp);
1204  tivabs.RefineUniformly(theL);
1205  //tivabs.Experiment().DWrite();
1206 
1207 
1208  // loop refine
1209  while(true) {
1210 
1211  // copy abstraction
1212  Generator abst=tivabs.TivAbstraction();
1213  abst.StateNamesEnabled(false);
1214  MarkAllStates(abst);
1215  abst.Name("overall abstraction");
1216 
1217  // report statistics
1218  tivabs.Experiment().SWrite();
1219  abst.Write("tmp_abs2.gen");
1220 
1221  std::cout << "################################\n";
1222  std::cout << "# cycle control synthesis \n";
1223  std::cout << "# ctrl evs " << uevents.ToString() << "\n";
1224  std::cout << "################################\n";
1225 
1226 
1227  // target specification by y (full automata)
1228  Generator spec;
1229  spec.InjectAlphabet(lioha.Alphabet());
1230  Idx s0=spec.InsInitState();
1231  Idx st=spec.InsMarkedState();
1232  spec.SetTransition(s0,spec.EventIndex("y_w"),st);
1233  spec.SetTransition(st,spec.EventIndex("y_w"),st);
1234  EventSet sfloop=lioha.Alphabet();
1235  sfloop.Erase("y_w");
1236  SelfLoop(spec,sfloop);
1237  spec.GraphWrite("tmp_spec.png");
1238 
1239  // hack : enforce to start with u
1240  /*
1241  Generator guy;
1242  guy.InjectAlphabet(lioha.Alphabet());
1243  Idx qu=guy.InsInitState();
1244  Idx qy=guy.InsState();
1245  MarkAllStates(guy);
1246  EventSet::Iterator eit=uevents.Begin();
1247  EventSet::Iterator eit_end=uevents.End();
1248  for(;eit!=eit_end;++eit)
1249  guy.SetTransition(qu,*eit,qy);
1250  eit=yevents.Begin();
1251  eit_end=yevents.End();
1252  for(;eit!=eit_end;++eit)
1253  guy.SetTransition(qy,*eit,qu);
1254  Parallel(spec,guy,spec);
1255  */
1256 
1257  // guide: do not use repeated inputs
1258  EventSet::Iterator eit=uevents.Begin();
1259  EventSet::Iterator eit_end=uevents.End();
1260  Generator guu;
1261  guu.InjectAlphabet(uevents);
1262  for(;eit!=eit_end;++eit)
1263  guu.InsState(*eit);
1264  Idx q0 = guu.InsInitState();
1265  eit=uevents.Begin();
1266  eit_end=uevents.End();
1267  for(;eit!=eit_end;++eit) {
1268  guu.SetTransition(q0,*eit,*eit);
1269  EventSet::Iterator eit2=uevents.Begin();
1270  EventSet::Iterator eit2_end=uevents.End();
1271  for(;eit2!=eit2_end;++eit2)
1272  if(*eit2!=*eit)
1273  guu.SetTransition(*eit,*eit2,*eit2);
1274  }
1275  MarkAllStates(guu);
1276  Parallel(spec,guu,spec);
1277 
1278 
1279  // patrol spec
1280  /*
1281  Generator spec;
1282  spec.InjectAlphabet(lioha.Alphabet());
1283  Idx sga=spec.InsInitState();
1284  Idx sgb=spec.InsState();
1285  Idx ssa=spec.InsMarkedState();
1286  Idx ssb=spec.InsMarkedState();
1287  spec.SetTransition(sga,spec.EventIndex("y_A"),ssa);
1288  spec.SetTransition(sga,spec.EventIndex("y_B"),sga);
1289  spec.SetTransition(ssa,spec.EventIndex("y_A"),sgb);
1290  spec.SetTransition(ssa,spec.EventIndex("y_B"),ssb);
1291  spec.SetTransition(sgb,spec.EventIndex("y_B"),ssb);
1292  spec.SetTransition(sgb,spec.EventIndex("y_A"),sgb);
1293  spec.SetTransition(ssb,spec.EventIndex("y_B"),sga);
1294  spec.SetTransition(ssb,spec.EventIndex("y_A"),ssa);
1295  EventSet other=lioha.Alphabet();
1296  other.Erase("y_A");
1297  other.Erase("y_B");
1298  EventSet::Iterator eit=other.Begin();
1299  for(;eit!=other.End();++eit) {
1300  spec.SetTransition(sga,*eit,sga);
1301  spec.SetTransition(ssa,*eit,sgb);
1302  spec.SetTransition(sgb,*eit,sgb);
1303  spec.SetTransition(ssb,*eit,sga);
1304  }
1305  spec.GraphWrite("tmp_spec.png");
1306  */
1307 
1308  // target control: reach marked state inf often
1309  Generator loop;
1310  ProductCompositionMap cmap_abst_spec;
1311  aProduct(abst,spec,cmap_abst_spec,loop);
1312  StateSet constraint = loop.States();
1313  StateSet winning;
1314  StateSet target;
1315 
1316  while(true) {
1317  target = loop.MarkedStates();
1318  target.RestrictSet(constraint);
1319  int csz=constraint.Size();
1320  int tsz=target.Size();
1321  std::cout << "target control: constraint #" << csz << " target #" << tsz << "\n";
1322  winning.Clear();
1323 
1324  while(true) {
1325  int wsz=winning.Size();
1326  std::cout << "target control: #" << wsz << " / #" << loop.Size() << "\n";
1327  StateSet ctrlreach;
1328  StateSet::Iterator sit=loop.StatesBegin();
1329  StateSet::Iterator sit_end=loop.StatesEnd();
1330  for(;sit!=sit_end;++sit) {
1331  if(winning.Exists(*sit)) continue;
1332  bool ok=false;
1333  TransSet::Iterator tit=loop.TransRelBegin(*sit);
1334  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
1335  for(;tit!=tit_end;++tit) {
1336  if(winning.Exists(tit->X2)) {ok=true; continue;}
1337  if(target.Exists(tit->X2)) {ok=true; continue;}
1338  if(uevents.Exists(tit->Ev)) continue;
1339  ok=false;
1340  break;
1341  }
1342  if(ok) ctrlreach.Insert(*sit);
1343  }
1344  winning.InsertSet(ctrlreach);
1345  if(winning.Size()==wsz) break;
1346  }
1347 
1348  constraint.RestrictSet(winning);
1349  if(csz==constraint.Size()) break;
1350  }
1351 
1352  std::cout << "target control: #" << winning.Size() << " / #" << loop.Size() << "\n";
1353  bool success=winning.Exists(loop.InitState());
1354  if(success)
1355  std::cout << "target control: success (init state #" << loop.InitState() << " found to be winning)\n";
1356  else
1357  std::cout << "target control: FAIL\n";
1358  if(success) {
1359  std::cout << "target control: preparing ctrl\n";
1360  StateSet::Iterator sit=loop.StatesBegin();
1361  StateSet::Iterator sit_end=loop.StatesEnd();
1362  for(;sit!=sit_end;++sit) {
1363  if(!winning.Exists(*sit)) continue;
1364  TransSet tremove;
1365  TransSet::Iterator tit=loop.TransRelBegin(*sit);
1366  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
1367  for(;tit!=tit_end;++tit) {
1368  // fixme: this is not quite correct
1369  if(winning.Exists(tit->X2)) {continue;}
1370  if(target.Exists(tit->X2)) {continue;}
1371  if(uevents.Exists(tit->Ev)) { tremove.Insert(*tit); continue; }
1372  std::cout << "synthesis: INTERNAL ERROR C";
1373  return 0;
1374  }
1375  tit=tremove.Begin();
1376  tit_end=tremove.End();
1377  for(;tit!=tit_end;++tit)
1378  loop.ClrTransition(*tit);
1379  }
1380  loop.Write("tmp_sup.gen");
1381  return 0;
1382  }
1383 
1384  // diagnose failure
1385  StateSet tivleaves;
1386  StateSet tivleaves_goodchance;
1387  StateSet::Iterator sit=loop.StatesBegin();
1388  StateSet::Iterator sit_end=loop.StatesEnd();
1389  for(;sit!=sit_end;++sit) {
1390  // ok done
1391  if(winning.Exists(*sit)) continue;
1392  // sort states
1393  Idx qtivabs = cmap_abst_spec.Arg1State(*sit);
1394  // allways refine
1395  if(tivabs.Experiment().IsLeave(qtivabs)) tivleaves.Insert(qtivabs);
1396  // is there a chance to win?
1397  TransSet::Iterator tit=loop.TransRelBegin(*sit);
1398  TransSet::Iterator tit_end=loop.TransRelEnd(*sit);
1399  for(;tit!=tit_end;++tit) {
1400  if(winning.Exists(tit->X2)) break;
1401  TransSet::Iterator tit2=loop.TransRelBegin(tit->X2);
1402  TransSet::Iterator tit2_end=loop.TransRelEnd(tit->X2);
1403  for(;tit2!=tit2_end;++tit2) {
1404  if(winning.Exists(tit2->X2)) break;
1405  }
1406  if(tit2!=tit2_end) break;
1407  }
1408  if(tit==tit_end) continue;
1409  if(tivabs.Experiment().IsLeave(qtivabs)) tivleaves_goodchance.Insert(qtivabs);
1410  }
1411  std::cout << "################################\n";
1412  std::cout << "# diagnosis\n";
1413  std::cout << "# tiv-leaves to refine #" << tivleaves.Size() << "/" << tivabs.Experiment().Leaves().Size() << "\n";
1414  std::cout << "# candidates with better chance #" << tivleaves_goodchance.Size() << "/" << tivabs.Experiment().Leaves().Size() << "\n";
1415  std::cout << "################################\n";
1416 
1417  // do refine
1418  std::cout << "################################\n";
1419  std::cout << "# refine\n";
1420  std::cout << "################################\n";
1421  sit=tivleaves_goodchance.Begin();
1422  sit_end=tivleaves_goodchance.End();
1423  int xsz=tivabs.Experiment().Size();
1424  for(;sit!=sit_end;++sit) {
1425  tivabs.RefineAt(*sit);
1426  }
1427  if(xsz==tivabs.Experiment().Size())
1428  {
1429  sit=tivleaves.Begin();
1430  sit_end=tivleaves.End();
1431  for(;sit!=sit_end;++sit) {
1432  tivabs.RefineAt(*sit);
1433  }
1434  }
1435 
1436  // loop refine/synthesis
1437  }
1438 
1439 
1440  // done
1441  return 0;
1442 }
1443 
1444 
1445 
1446 // choose version
1447 int main() {
1448  //return robot2017();
1449  //return robot2018ti();
1450  return marine2018();
1451 }
faudes::Experiment
Finite fragment of a computation tree.
Definition: hyb_experiment.h:44
faudes::Experiment::InitialStates
void InitialStates(CompatibleStates *istates)
Definition: hyb_experiment.cpp:50
faudes::HybridStateSet
Set of states in an hybrid automata.
Definition: hyb_reachability.h:33
faudes::HybridStateSet::DWrite
void DWrite(const LinearHybridAutomaton &lha)
inspect
Definition: hyb_reachability.cpp:134
faudes::HybridStateSet::LocationsBegin
IndexSet::Iterator LocationsBegin(void) const
Definition: hyb_reachability.cpp:79
faudes::HybridStateSet::Assign
void Assign(const HybridStateSet &rOther)
assignment
Definition: hyb_reachability.cpp:50
faudes::HybridStateSet::Insert
void Insert(Idx q)
insert / erase (we take owvership of polyhedra)
Definition: hyb_reachability.cpp:97
faudes::HybridStateSet::LocationsEnd
IndexSet::Iterator LocationsEnd(void) const
Definition: hyb_reachability.cpp:82
faudes::IndexSet
Set of indices.
Definition: cfl_indexset.h:78
faudes::IndexSet::Insert
Idx Insert(void)
Insert new index to set.
Definition: cfl_indexset.cpp:313
faudes::LbdAbstraction::RefineUniformly
void RefineUniformly(unsigned int depth)
Definition: hyb_abstraction.cpp:47
faudes::LbdAbstraction::TivAbstraction
const Generator & TivAbstraction(void)
Definition: hyb_abstraction.cpp:55
faudes::LbdAbstraction::TvAbstraction
const Generator & TvAbstraction(void)
Definition: hyb_abstraction.cpp:65
faudes::LbdAbstraction::Experiment
void Experiment(faudes::Experiment *exp)
Definition: hyb_abstraction.cpp:26
faudes::Matrix
Matrix of scalars.
Definition: hyb_parameter.h:64
faudes::Matrix::At
const Scalar::Type & At(int i, int j) const
Get entry.
Definition: hyb_parameter.cpp:194
faudes::Matrix::Zero
void Zero(int rc=-1, int cc=-1)
Set to zero matrix.
Definition: hyb_parameter.cpp:172
faudes::NameSet
Set of indices with symbolic names.
Definition: cfl_nameset.h:69
faudes::NameSet::Exists
bool Exists(const Idx &rIndex) const
Test existence of index.
Definition: cfl_nameset.cpp:433
faudes::NameSet::SymbolicName
void SymbolicName(Idx index, const std::string &rName)
Set new name for existing index.
Definition: cfl_nameset.cpp:400
faudes::NameSet::Insert
bool Insert(const Idx &rIndex)
Add an element by index.
Definition: cfl_nameset.cpp:256
faudes::NameSet::EraseSet
void EraseSet(const NameSet &rOtherSet)
Erase elements specified by rOtherSet.
Definition: cfl_nameset.cpp:352
faudes::NameSet::Erase
virtual bool Erase(const Idx &rIndex)
Delete element by index.
Definition: cfl_nameset.cpp:308
faudes::Polyhedron
Polyhedron in R^n.
Definition: hyb_parameter.h:674
faudes::Polyhedron::AB
void AB(const Matrix &rA, const Vector &rB)
Set A matrix and B vector.
Definition: hyb_parameter.cpp:703
faudes::Polyhedron::Name
virtual const std::string & Name(void) const
Object name.
Definition: hyb_parameter.h:717
faudes::ProductCompositionMap
Rti-wrapper for composition maps.
Definition: cfl_parallel.h:43
faudes::ProductCompositionMap::Arg1State
Idx Arg1State(Idx s12) const
Definition: cfl_parallel.cpp:768
faudes::ProductCompositionMap::Arg2State
Idx Arg2State(Idx s12) const
Definition: cfl_parallel.cpp:785
faudes::TTransSet::Begin
Iterator Begin(void) const
Iterator to begin of set.
Definition: cfl_transset.h:1264
faudes::TTransSet::End
Iterator End(void) const
Iterator to end of set.
Definition: cfl_transset.h:1269
faudes::TTransSet::Insert
bool Insert(const Transition &rTransition)
Add a Transition.
Definition: cfl_transset.h:1470
faudes::TTransSet< TransSort::X1EvX2 >::Iterator
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Iterator on transition.
Definition: cfl_transset.h:269
faudes::TaGenerator::InsState
Idx InsState(void)
Add new anonymous state to generator.
Definition: cfl_agenerator.h:1118
faudes::TaGenerator::InsEvent
bool InsEvent(Idx index)
Add an existing event to alphabet by index.
Definition: cfl_agenerator.h:1094
faudes::TaGenerator::Alphabet
const TaEventSet< EventAttr > & Alphabet(void) const
Return const reference to alphabet.
Definition: cfl_agenerator.h:1358
faudes::TaGenerator::SetTransition
bool SetTransition(Idx x1, Idx ev, Idx x2)
Add a transition to generator by indices.
Definition: cfl_agenerator.h:1197
faudes::TlhaGenerator
Generator with linear hybrid automata extensions.
Definition: hyb_hgenerator.h:236
faudes::TlhaGenerator::Valid
virtual bool Valid(void) const
Check if generator is valid.
Definition: hyb_hgenerator.h:981
faudes::TlhaGenerator::Rate
const Polyhedron & Rate(Idx idx) const
Get rate of state by index.
Definition: hyb_hgenerator.h:851
faudes::TlhaGenerator::InitialConstraint
const Polyhedron & InitialConstraint(Idx idx) const
Get initial constraint of state by index.
Definition: hyb_hgenerator.h:800
faudes::TlhaGenerator::StateSpace
const Polyhedron & StateSpace(void) const
Get continuous statespace.
Definition: hyb_hgenerator.h:735
faudes::TlhaGenerator::Guard
const Polyhedron & Guard(const Transition &rTrans) const
Get guard of a transition.
Definition: hyb_hgenerator.h:900
faudes::TlhaGenerator::Invariant
const Polyhedron & Invariant(Idx idx) const
Get invariant of state by index.
Definition: hyb_hgenerator.h:751
faudes::Transition
Triple (X1,Ev,X2) to represent current state, event and next state.
Definition: cfl_transset.h:57
faudes::Type::ToString
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Write configuration data to a string.
Definition: cfl_types.cpp:169
faudes::Type::Write
void Write(const Type *pContext=0) const
Write configuration data to console.
Definition: cfl_types.cpp:139
faudes::Type::SWrite
void SWrite(TokenWriter &rTw) const
Write statistics comment to TokenWriter.
Definition: cfl_types.cpp:256
faudes::Vector
Vector of scalars.
Definition: hyb_parameter.h:391
faudes::Vector::At
const Scalar::Type & At(int i) const
Get entry.
Definition: hyb_parameter.cpp:455
faudes::Vector::Zero
void Zero(int dim=-1)
Set to zero vector.
Definition: hyb_parameter.cpp:441
faudes::vGenerator
Base class of all FAUDES generators.
Definition: cfl_generator.h:213
faudes::vGenerator::StatesBegin
StateSet::Iterator StatesBegin(void) const
Iterator to Begin() of state set.
Definition: cfl_generator.cpp:1057
faudes::vGenerator::InitStatesBegin
StateSet::Iterator InitStatesBegin(void) const
Iterator to Begin() of mInitStates.
Definition: cfl_generator.cpp:1150
faudes::vGenerator::SetTransition
bool SetTransition(Idx x1, Idx ev, Idx x2)
Add a transition to generator by indices.
Definition: cfl_generator.cpp:1626
faudes::vGenerator::MarkedStates
const StateSet & MarkedStates(void) const
Return const ref of marked states.
Definition: cfl_generator.cpp:1913
faudes::vGenerator::InsMarkedState
Idx InsMarkedState(void)
Create new anonymous state and set as marked state.
Definition: cfl_generator.cpp:1318
faudes::vGenerator::TransRelBegin
TransSet::Iterator TransRelBegin(void) const
Iterator to Begin() of transition relation.
Definition: cfl_generator.cpp:1067
faudes::vGenerator::ClrTransition
void ClrTransition(Idx x1, Idx ev, Idx x2)
Remove a transition by indices.
Definition: cfl_generator.cpp:1660
faudes::vGenerator::StateIndex
Idx StateIndex(const std::string &rName) const
State index lookup.
Definition: cfl_generator.cpp:944
faudes::vGenerator::InsEvents
void InsEvents(const EventSet &events)
Add new named events to generator.
Definition: cfl_generator.cpp:1210
faudes::vGenerator::EventIndex
Idx EventIndex(const std::string &rName) const
Event index lookup.
Definition: cfl_generator.cpp:834
faudes::vGenerator::TStr
std::string TStr(const Transition &rTrans) const
Return pretty printable transition (eg for debugging)
Definition: cfl_generator.cpp:3841
faudes::vGenerator::Name
void Name(const std::string &rName)
Set the generator's name.
Definition: cfl_generator.cpp:526
faudes::vGenerator::StatesEnd
StateSet::Iterator StatesEnd(void) const
Iterator to End() of state set.
Definition: cfl_generator.cpp:1062
faudes::vGenerator::TransRelEnd
TransSet::Iterator TransRelEnd(void) const
Iterator to End() of transition relation.
Definition: cfl_generator.cpp:1072
faudes::vGenerator::ExistsEvent
bool ExistsEvent(Idx index) const
Test existence of event in alphabet.
Definition: cfl_generator.cpp:1756
faudes::vGenerator::EStr
std::string EStr(Idx index) const
Pretty printable event name for index (eg for debugging).
Definition: cfl_generator.cpp:3828
faudes::vGenerator::InsState
Idx InsState(void)
Add new anonymous state to generator.
Definition: cfl_generator.cpp:1247
faudes::vGenerator::InitState
Idx InitState(void) const
Return initial state.
Definition: cfl_generator.cpp:1142
faudes::vGenerator::InsInitState
Idx InsInitState(void)
Create new anonymous state and set as initial state.
Definition: cfl_generator.cpp:1287
faudes::vGenerator::StateNamesEnabled
bool StateNamesEnabled(void) const
Whether libFAUEDS functions are requested to generate state names.
Definition: cfl_generator.cpp:999
faudes::vGenerator::InitStatesEnd
StateSet::Iterator InitStatesEnd(void) const
Iterator to End() of mInitStates.
Definition: cfl_generator.cpp:1155
faudes::vGenerator::GraphWrite
void GraphWrite(const std::string &rFileName, const std::string &rOutFormat="", const std::string &rDotExec="dot") const
Produce graphical representation of this generator.
Definition: cfl_generator.cpp:3847
faudes::vGenerator::Size
Idx Size(void) const
Get generator size (number of states)
Definition: cfl_generator.cpp:577
faudes::vGenerator::States
const StateSet & States(void) const
Return reference to state set.
Definition: cfl_generator.cpp:1883
faudes::vGenerator::InjectAlphabet
void InjectAlphabet(const EventSet &rNewalphabet)
Set mpAlphabet without consistency check.
Definition: cfl_generator.cpp:1170
faudes::TBaseSet::Exists
bool Exists(const T &rElem) const
Test existence of element.
Definition: cfl_baseset.h:2115
faudes::TBaseSet::Clear
virtual void Clear(void)
Clear all set.
Definition: cfl_baseset.h:1902
faudes::TBaseSet::End
Iterator End(void) const
Iterator to the end of set.
Definition: cfl_baseset.h:1896
faudes::TBaseSet::RestrictSet
virtual void RestrictSet(const TBaseSet &rOtherSet)
Restrict elements given by other set.
Definition: cfl_baseset.h:2064
faudes::TBaseSet::InsertSet
virtual void InsertSet(const TBaseSet &rOtherSet)
Insert elements given by rOtherSet.
Definition: cfl_baseset.h:1987
faudes::TBaseSet::Begin
Iterator Begin(void) const
Iterator to the begin of set.
Definition: cfl_baseset.h:1891
faudes::TBaseSet::Size
Idx Size(void) const
Get Size of TBaseSet.
Definition: cfl_baseset.h:1819
faudes::SelfLoop
void SelfLoop(Generator &rGen, const EventSet &rAlphabet)
Self-loop all states.
Definition: cfl_regular.cpp:1003
faudes::aProduct
void aProduct(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Product composition.
Definition: cfl_parallel.cpp:426
faudes::MarkAllStates
void MarkAllStates(vGenerator &rGen)
RTI wrapper function.
Definition: cfl_generator.cpp:3986
faudes::Parallel
void Parallel(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Parallel composition.
Definition: cfl_parallel.cpp:32
faudes::PolyFinalise
void PolyFinalise(const Polyhedron &fpoly)
convert PPL polyhedron back to faudes data structures; this is required if we manipulate a polyhedron...
Definition: hyb_compute.cpp:53
faudes::PolyIntersection
void PolyIntersection(const Polyhedron &poly, Polyhedron &res)
intersection
Definition: hyb_compute.cpp:176
execute
int execute(LinearHybridAutomaton &plant, HybridStateSet &cstates)
Definition: hyb_6_robotex.cpp:609
robot
void robot(int szi, int szj, int mesh, int overlap, int disturbance, LinearHybridAutomaton &harobot, EventSet &uevents)
Definition: hyb_6_robotex.cpp:25
robot2018ti
int robot2018ti()
Run the tutorial: time invariant robot.
Definition: hyb_6_robotex.cpp:940
marine2018
int marine2018()
Run the tutorial: time invariant marine.
Definition: hyb_6_robotex.cpp:1153
robot2017
int robot2017()
Run the tutorial: time variant robot, target control.
Definition: hyb_6_robotex.cpp:689
main
int main()
Definition: hyb_6_robotex.cpp:1447
marine
void marine(int width, int height, int overlap, int velocity, int disturbance, LinearHybridAutomaton &hamarine, EventSet &uevents)
Definition: hyb_6_robotex.cpp:405
hyb_compute.h
libfaudes.h
Includes all libFAUDES headers, incl plugings
faudes
libFAUDES resides within the namespace faudes.
Definition: cfl_agenerator.h:43
faudes::Idx
uint32_t Idx
Type definition for index type (allways 32bit)
Definition: cfl_definitions.h:43
faudes::ToIdx
Idx ToIdx(const std::string &rString)
Convert a string to Idx.
Definition: cfl_helper.cpp:100
faudes::LhaReach
void LhaReach(const LinearHybridAutomaton &lha, const HybridStateSet &states, std::map< Idx, HybridStateSet * > &ostates, int *pCnt)
compute sets of reachable state per successor event
Definition: hyb_reachability.cpp:163

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

>>