hyb_6_robotex.cpp
Go to the documentation of this file.
1/** @file hyb_6_robotex.cpp
2
3Tutorial, hybrid systems plugin.
4This tutorial sets up the patrol robot example and synthesises
5a simple controller. It is used in a WODES and in a JDEDS
6submission.
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
18using 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
25void 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 */
405void 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 */
609int 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.Copy(*sit->second);
682
683 // report event
684 return sit->first;
685}
686
687
688/** Run the tutorial: time variant robot, target control */
689int 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.Copy(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 */
940int 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.Copy(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 */
1153int 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.Copy(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
1447int main() {
1448 //return robot2017();
1449 //return robot2018ti();
1450 return marine2018();
1451}
faudes::Experiment::InitialStates
void InitialStates(CompatibleStates *istates)
Definition hyb_experiment.cpp:50
faudes::ExtType::Name
const std::string & Name(void) const
Definition cfl_types.cpp:443
faudes::HybridStateSet::Copy
void Copy(const HybridStateSet &rOther)
Definition hyb_reachability.cpp:50
faudes::HybridStateSet::DWrite
void DWrite(const LinearHybridAutomaton &lha)
Definition hyb_reachability.cpp:134
faudes::HybridStateSet::LocationsBegin
IndexSet::Iterator LocationsBegin(void) const
Definition hyb_reachability.cpp:79
faudes::HybridStateSet::LocationsEnd
IndexSet::Iterator LocationsEnd(void) const
Definition hyb_reachability.cpp:82
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::At
const Scalar::Type & At(int i, int j) const
Definition hyb_parameter.cpp:194
faudes::Matrix::Zero
void Zero(int rc=-1, int cc=-1)
Definition hyb_parameter.cpp:172
faudes::NameSet::Exists
bool Exists(const Idx &rIndex) const
Definition cfl_nameset.cpp:452
faudes::NameSet::SymbolicName
void SymbolicName(Idx index, const std::string &rName)
Definition cfl_nameset.cpp:419
faudes::NameSet::Insert
bool Insert(const Idx &rIndex)
Definition cfl_nameset.cpp:275
faudes::NameSet::EraseSet
void EraseSet(const NameSet &rOtherSet)
Definition cfl_nameset.cpp:371
faudes::NameSet::Erase
virtual bool Erase(const Idx &rIndex)
Definition cfl_nameset.cpp:327
faudes::Polyhedron::Name
virtual const std::string & Name(void) const
Definition hyb_parameter.h:717
faudes::Polyhedron::AB
void AB(const Matrix &rA, const Vector &rB)
Definition hyb_parameter.cpp:703
faudes::TTransSet::Begin
Iterator Begin(void) const
Definition cfl_transset.h:1374
faudes::TTransSet::End
Iterator End(void) const
Definition cfl_transset.h:1379
faudes::TTransSet< TransSort::X1EvX2 >::Iterator
TBaseSet< Transition, TransSort::X1EvX2 >::Iterator Iterator
Definition cfl_transset.h:279
faudes::TTransSet::Insert
bool Insert(const Transition &rTransition)
Definition cfl_transset.h:1580
faudes::TaGenerator::InsEvent
bool InsEvent(Idx index)
Definition cfl_agenerator.h:1079
faudes::TaGenerator::Alphabet
const TaEventSet< EventAttr > & Alphabet(void) const
Definition cfl_agenerator.h:1343
faudes::TaGenerator::SetTransition
bool SetTransition(Idx x1, Idx ev, Idx x2)
Definition cfl_agenerator.h:1182
faudes::TlhaGenerator::Valid
virtual bool Valid(void) const
Definition hyb_hgenerator.h:981
faudes::TlhaGenerator::Rate
const Polyhedron & Rate(Idx idx) const
Definition hyb_hgenerator.h:851
faudes::TlhaGenerator::InitialConstraint
const Polyhedron & InitialConstraint(Idx idx) const
Definition hyb_hgenerator.h:800
faudes::TlhaGenerator::StateSpace
const Polyhedron & StateSpace(void) const
Definition hyb_hgenerator.h:735
faudes::TlhaGenerator::Guard
const Polyhedron & Guard(const Transition &rTrans) const
Definition hyb_hgenerator.h:900
faudes::TlhaGenerator::Invariant
const Polyhedron & Invariant(Idx idx) const
Definition hyb_hgenerator.h:751
faudes::Type::ToString
std::string ToString(const std::string &rLabel="", const Type *pContext=0) const
Definition cfl_types.cpp:196
faudes::Type::Write
void Write(const Type *pContext=0) const
Definition cfl_types.cpp:166
faudes::Type::SWrite
void SWrite(TokenWriter &rTw) const
Definition cfl_types.cpp:283
faudes::Vector::At
const Scalar::Type & At(int i) const
Definition hyb_parameter.cpp:455
faudes::Vector::Zero
void Zero(int dim=-1)
Definition hyb_parameter.cpp:441
faudes::vGenerator::StatesBegin
StateSet::Iterator StatesBegin(void) const
Definition cfl_generator.cpp:1079
faudes::vGenerator::InitStatesBegin
StateSet::Iterator InitStatesBegin(void) const
Definition cfl_generator.cpp:1172
faudes::vGenerator::SetTransition
bool SetTransition(Idx x1, Idx ev, Idx x2)
Definition cfl_generator.cpp:1648
faudes::vGenerator::MarkedStates
const StateSet & MarkedStates(void) const
Definition cfl_generator.cpp:1935
faudes::vGenerator::TransRelBegin
TransSet::Iterator TransRelBegin(void) const
Definition cfl_generator.cpp:1089
faudes::vGenerator::ClrTransition
void ClrTransition(Idx x1, Idx ev, Idx x2)
Definition cfl_generator.cpp:1682
faudes::vGenerator::StateIndex
Idx StateIndex(const std::string &rName) const
Definition cfl_generator.cpp:966
faudes::vGenerator::InsEvents
void InsEvents(const EventSet &events)
Definition cfl_generator.cpp:1232
faudes::vGenerator::EventIndex
Idx EventIndex(const std::string &rName) const
Definition cfl_generator.cpp:856
faudes::vGenerator::TStr
std::string TStr(const Transition &rTrans) const
Definition cfl_generator.cpp:3970
faudes::vGenerator::StatesEnd
StateSet::Iterator StatesEnd(void) const
Definition cfl_generator.cpp:1084
faudes::vGenerator::TransRelEnd
TransSet::Iterator TransRelEnd(void) const
Definition cfl_generator.cpp:1094
faudes::vGenerator::ExistsEvent
bool ExistsEvent(Idx index) const
Definition cfl_generator.cpp:1778
faudes::vGenerator::EStr
std::string EStr(Idx index) const
Definition cfl_generator.cpp:3957
faudes::vGenerator::InitState
Idx InitState(void) const
Definition cfl_generator.cpp:1164
faudes::vGenerator::StateNamesEnabled
bool StateNamesEnabled(void) const
Definition cfl_generator.cpp:1021
faudes::vGenerator::InitStatesEnd
StateSet::Iterator InitStatesEnd(void) const
Definition cfl_generator.cpp:1177
faudes::vGenerator::GraphWrite
void GraphWrite(const std::string &rFileName, const std::string &rOutFormat="", const std::string &rDotExec="dot") const
Definition cfl_generator.cpp:3976
faudes::vGenerator::Size
Idx Size(void) const
Definition cfl_generator.cpp:599
faudes::vGenerator::States
const StateSet & States(void) const
Definition cfl_generator.cpp:1905
faudes::vGenerator::InjectAlphabet
void InjectAlphabet(const EventSet &rNewalphabet)
Definition cfl_generator.cpp:1192
faudes::TBaseSet::Exists
bool Exists(const T &rElem) const
Definition cfl_baseset.h:2333
faudes::TBaseSet::Clear
virtual void Clear(void)
Definition cfl_baseset.h:2115
faudes::TBaseSet::End
Iterator End(void) const
Definition cfl_baseset.h:2109
faudes::TBaseSet::RestrictSet
virtual void RestrictSet(const TBaseSet &rOtherSet)
Definition cfl_baseset.h:2282
faudes::TBaseSet::InsertSet
virtual void InsertSet(const TBaseSet &rOtherSet)
Definition cfl_baseset.h:2205
faudes::TBaseSet::Begin
Iterator Begin(void) const
Definition cfl_baseset.h:2104
faudes::TBaseSet::Size
Idx Size(void) const
Definition cfl_baseset.h:1910
faudes::SelfLoop
void SelfLoop(Generator &rGen, const EventSet &rAlphabet)
Definition cfl_regular.cpp:1034
faudes::aProduct
void aProduct(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Definition cfl_parallel.cpp:527
faudes::MarkAllStates
void MarkAllStates(vGenerator &rGen)
Definition cfl_generator.cpp:4101
faudes::Parallel
void Parallel(const Generator &rGen1, const Generator &rGen2, Generator &rResGen)
Definition cfl_parallel.cpp:33
faudes::PolyFinalise
void PolyFinalise(const Polyhedron &fpoly)
Definition hyb_compute.cpp:53
faudes::PolyIntersection
void PolyIntersection(const Polyhedron &poly, Polyhedron &res)
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()
Definition hyb_6_robotex.cpp:940
marine2018
int marine2018()
Definition hyb_6_robotex.cpp:1153
robot2017
int robot2017()
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
faudes::Idx
uint32_t Idx
Definition cfl_definitions.h:43
faudes::ToIdx
Idx ToIdx(const std::string &rString)
Definition cfl_utils.cpp:100
faudes::LhaReach
void LhaReach(const LinearHybridAutomaton &lha, const HybridStateSet &states, std::map< Idx, HybridStateSet * > &ostates, int *pCnt)
Definition hyb_reachability.cpp:163

libFAUDES 2.34d --- 2026.03.11 --- c++ api documentaion by doxygen

>>