diff --git a/lab3/README.md b/lab3/README.md new file mode 100644 index 0000000..a0cfc63 --- /dev/null +++ b/lab3/README.md @@ -0,0 +1,18 @@ +# CPS Lab 3 Exercise (2021-12-22) + +- Mariano Sciacco +- Federico Carboni +- Giuseppe Rossano +- Alessandro Benetti + +## Notes + +> Note 1: requires `gnuplot` and `phaverlite` (see https://www.cs.unipr.it/~zaffanella/PPLite/PHAVerLite) + +> Note 2: all credits to `phaver` executable in this folder goes to Enea Zaffanella + +> Note 3: execute `./phaver ` to compile the `.pha` file + +> Note 4: execute `gnuplot --persist -c phaverplot.gp filename.txt` to generate the graph + +> Note 5: results of the plot are inside the respective folders as pdf files. diff --git a/lab3/examples/bouncing.pha b/lab3/examples/bouncing.pha new file mode 100644 index 0000000..d41b27e --- /dev/null +++ b/lab3/examples/bouncing.pha @@ -0,0 +1,57 @@ +// ---------------------------------------------------------- +// Hybrid System Example: Bouncing Ball +// ---------------------------------------------------------- + +// ---------------------------------------------------------- +// Constants +// ---------------------------------------------------------- +g:=1; // constant for gravity + +// ---------------------------------------------------------- +// System Description +// ---------------------------------------------------------- +automaton bouncing_ball +contr_var: v, x; +synclabs: jump; +loc state: while x>=0 & x<=10 & v<=10 & v>=-10 wait {x'==v & v'==-g} + when x==0 & v<0 sync jump do {v'==-v*0.5 & x'==x} goto state; +initially: state & x==2 & v==0; +end + +// ---------------------------------------------------------- +// Define Partitioning +// ---------------------------------------------------------- +// Add a new label for the transitions that are introduced +// between partitions +bouncing_ball.add_label(tau); + +// Define the directions of the partitions +// here: in both axes with a min. threshold of partition size 0.2 +bouncing_ball.set_refine_constraints((x, 0.2),(v,0.2),tau); + +// With this partitioning we can use convex hull overapproximations, +// resulting in fewer polyhedra (one per partition) +//REACH_USE_CONVEX_HULL=true; + +// ---------------------------------------------------------- +// Define Partitioning (alternative) +// ---------------------------------------------------------- +// We can also just partition in the v-direction, but then we must turn off +// the convex hull (try it...) +// bouncing_ball.set_refine_constraints((v,0.2),tau); +// REACH_USE_CONVEX_HULL=false; + +// ---------------------------------------------------------- +// Analysis Commands +// ---------------------------------------------------------- +reg=bouncing_ball.reachable; + +// ---------------------------------------------------------- +// Saving Data for Graphical Output +// ---------------------------------------------------------- +reg.print("out_reach",2); // output as a list of vertices + +// for display with graph use, e.g.: +// graph -T X -C -B -q0.5 out_reach +// for display with matlab use, e.g.: +// plot_2d_vertices('out_m_reach') diff --git a/lab3/examples/bouncing_timed.pha b/lab3/examples/bouncing_timed.pha new file mode 100644 index 0000000..138e5b0 --- /dev/null +++ b/lab3/examples/bouncing_timed.pha @@ -0,0 +1,81 @@ +// ---------------------------------------------------------- +// Hybrid System Example: Bouncing Ball +// ---------------------------------------------------------- +// This version produces a plot of position over time. +// A clock is added to the system to model time explicitly. +// This gives us a another choice of partitioning: along +// the time-axis. It's fast, but doesn't work with convex +// hull. +// +// The complexity of this example requires us to put limits +// on the bits used in polyhedral computations. +// Otherwise, it may take very long or not terminate at all. +REACH_CONSTRAINT_LIMIT = 48; +REACH_CONSTRAINT_TRIGGER = 96; +CONSTRAINT_BITSIZE = 24; +REACH_BITSIZE_TRIGGER = 200; +// ---------------------------------------------------------- +// Constants +// ---------------------------------------------------------- +g:=1; // constant for gravity + +// ---------------------------------------------------------- +// System Description +// ---------------------------------------------------------- +automaton bouncing_ball +contr_var: t, x, v; +synclabs: jump; +loc state: while x>=0 & x<=10 & v<=10 & v>=-10 & t<=5 & t>=0 wait {x'==v & v'==-g & t'==1} + when x==0 & v<0 sync jump do {v'==-v*0.5 & x'==x & t'==t} goto state; +initially: state & x==2 & v==0 & t==0; +end + +// ---------------------------------------------------------- +// Define Partitioning +// ---------------------------------------------------------- +// Add a new label for the transitions that are introduced +// between partitions +bouncing_ball.add_label(tau); + +// Define the directions of the partitions +// here: in both axes with a min. threshold of partition size 0.2 +bouncing_ball.set_refine_constraints((x, 0.2),(v,0.2),tau); + +// With this partitioning we can use convex hull overapproximations, +// resulting in fewer polyhedra (one per partition) +//REACH_USE_CONVEX_HULL=true; + +// ---------------------------------------------------------- +// Define Partitioning (alternative 1) +// ---------------------------------------------------------- +// We can also just partition in the v-direction, but then +// we must turn off convex hull (try it...) +// bouncing_ball.set_refine_constraints((v,0.2),tau); +// REACH_USE_CONVEX_HULL=false; + +// ---------------------------------------------------------- +// Define Partitioning (alternative 2) +// ---------------------------------------------------------- +// We can also just partition in the t-direction, but then +// we must turn off convex hull +// and refine the time-elapse operator at least twice +// at every step (try it...) +//TIME_POST_ITER=2; +//bouncing_ball.set_refine_constraints((t, 0.1),tau); +//REACH_USE_CONVEX_HULL=false; + +// ---------------------------------------------------------- +// Analysis Commands +// ---------------------------------------------------------- +reg=bouncing_ball.reachable; + +// ---------------------------------------------------------- +// Saving Data for Graphical Output +// ---------------------------------------------------------- +reg.project_to(t, x); // remove v to get a 2-dim output +reg.print("out_reach",2); // output as a list of vertices + +// for display with graph use, e.g.: +// graph -T X -C -B -q0.5 out_reach +// for display with matlab use, e.g.: +// plot_2d_vertices('out_m_reach') diff --git a/lab3/examples/evader.pha b/lab3/examples/evader.pha new file mode 100644 index 0000000..78cebca --- /dev/null +++ b/lab3/examples/evader.pha @@ -0,0 +1,63 @@ +// Constants definition +// + +// Automaton definition +// +automaton evader +contr_var: e, p, x; // e position of the evader + // p position of the pursuer + // x timer +synclabs: jump; +loc ClkW: + while 0 <= e <= 40 & 0 <= p <= 40 & x <= 2 wait + {e'==5 & -0.5 <= p' <= 6 & x'==1} + when (p == 0) sync jump do {e'==e & p'==40 & x'==x} goto ClkW; + when (p == 40) sync jump do {e'==e & p'==0 & x'==x} goto ClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p > 40) sync jump do + {e'==e & p'==p & x'==0} goto ClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p <= 40) sync jump do + {e'==e & p'==p & x'==0} goto CntrClkW; + when (e == 0) sync jump do {e'==e & p'==p & x'==x} goto Rescued; + when (e == 40) sync jump do {e'==e & p'==p & x'==x} goto Rescued; +loc CntrClkW: + while 0 <= e <= 40 & 0 <= p <= 40 & x <= 2 wait + {e'==-5 & -0.5 <= p' <= 6 & x'==1} + when (p == 0) sync jump do {e'==e & p'==40 & x'==x} goto CntrClkW; + when (p == 40) sync jump do {e'==e & p'==0 & x'==x} goto CntrClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p > 40) sync jump do + {e'==e & p'==p & x'==0} goto ClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p <= 40) sync jump do + {e'==e & p'==p & x'==0} goto CntrClkW; + when (e == 0) sync jump do {e'==e & p'==p & x'==x} goto Rescued; + when (e == 40) sync jump do {e'==e & p'==p & x'==x} goto Rescued; +loc Rescued: + while true wait {e'==0 & p'==0 & x'==0 }; + +initially: ClkW & x == 2 & e == 20 & p == 10; +end + +// Compute the reachable set +// +region=evader.reachable; +// +// Output to file +// +// List regions (pairs of locations names and linear formulas) +region.print("evader_regions.txt", 0); +// Sequence of vertices in floating point form. +// Can be plotted with gnuplot +// Project on e and p +region.project_to(e, p); +region.print("evader.txt", 2); + +// Safety verification +// +// definition of bad states +forbidden = evader.{$ & e == p}; +reach_set = evader.is_reachable(forbidden); +reach_set.intersection_assign(forbidden); + +echo "The intersection between the reachable set and the bad region is:"; +reach_set.is_empty; + + \ No newline at end of file diff --git a/lab3/examples/evader2.pha b/lab3/examples/evader2.pha new file mode 100644 index 0000000..bb2a5a0 --- /dev/null +++ b/lab3/examples/evader2.pha @@ -0,0 +1,59 @@ +// Constants definition +// + +// Automaton definition +// +automaton evader +contr_var: e, p, x, p_zero; // e position of the evader + // p position of the pursuer + // x timer + // p_zero "frozen variable" that stores the + // initial position of the pursuer +synclabs: jump; +loc ClkW: + while 0 <= e <= 40 & 0 <= p <= 40 & x <= 2 wait + {e'==5 & -0.5 <= p' <= 6 & x'==1 & p_zero'==0} + when (p == 0) sync jump do {e'==e & p'==40 & x'==x & p_zero'==p_zero} goto ClkW; + when (p == 40) sync jump do {e'==e & p'==0 & x'==x & p_zero'==p_zero} goto ClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p > 40) sync jump do + {e'==e & p'==p & x'==0 & p_zero'==p_zero} goto ClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p <= 40) sync jump do + {e'==e & p'==p & x'==0 & p_zero'==p_zero} goto CntrClkW; + when (e == 0) sync jump do {e'==e & p'==p & x'==x & p_zero'==p_zero} goto Rescued; + when (e == 40) sync jump do {e'==e & p'==p & x'==x & p_zero'==p_zero} goto Rescued; +loc CntrClkW: + while 0 <= e <= 40 & 0 <= p <= 40 & x <= 2 wait + {e'==-5 & -0.5 <= p' <= 6 & x'==1 & p_zero'==0} + when (p == 0) sync jump do {e'==e & p'==40 & x'==x & p_zero'==p_zero} goto CntrClkW; + when (p == 40) sync jump do {e'==e & p'==0 & x'==x & p_zero'==p_zero} goto CntrClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p > 40) sync jump do + {e'==e & p'==p & x'==0 & p_zero'==p_zero} goto ClkW; + when (x >= 2) & (0 < e < 40) & (6*e - 5*p <= 40) sync jump do + {e'==e & p'==p & x'==0 & p_zero'==p_zero} goto CntrClkW; + when (e == 0) sync jump do {e'==e & p'==p & x'==x & p_zero'==p_zero} goto Rescued; + when (e == 40) sync jump do {e'==e & p'==p & x'==x & p_zero'==p_zero} goto Rescued; +loc Rescued: + while true wait {e'==0 & p'==0 & x'==0 & p_zero'==0}; + +initially: ClkW & x == 2 & e == 20 & p == p_zero & 0 <= p <= 40; +end + +// Find winning starting points for pursuer +// +// Compute the reachable set +// +region=evader.reachable; +// Intersect with states where pursuer wins +forbidden = evader.{$ & e == p}; +region.intersection_assign(forbidden); +// Project on p_zero to get the initial position for the pursuer for which the +// pursuer can win the game +region.project_to(p_zero); +// union over all locations +pursuer_wins = region.loc_union; + +echo "The pursuer can win the game if it starts from:"; +pursuer_wins.print; + + + \ No newline at end of file diff --git a/lab3/examples/txt/evader.txt b/lab3/examples/txt/evader.txt new file mode 100644 index 0000000..dee27fb --- /dev/null +++ b/lab3/examples/txt/evader.txt @@ -0,0 +1,16 @@ +20 10 + +20 10 +30 9 +30 22 +20 10 + +30 22 +30 9 +40 8 +40 34 +30 22 + +40 8 +40 34 + diff --git a/lab3/examples/txt/evader_regions.txt b/lab3/examples/txt/evader_regions.txt new file mode 100644 index 0000000..5a1dd67 --- /dev/null +++ b/lab3/examples/txt/evader_regions.txt @@ -0,0 +1,4 @@ +region = evader.{ +ClkW & (x == 2 & p == 10 & e == 20 | e == 5*x + 20 & 6*e >= 5*p + 70 & e + 10*p >= 120 & e <= 30 | e == 5*x + 30 & e + 10*p >= 120 & 30 <= e <= 40 & 6*e >= 5*p + 70), +Rescued & x == 2 & e == 40 & 8 <= p <= 34 +}; \ No newline at end of file diff --git a/lab3/exercise/ex1.1/lake.pdf b/lab3/exercise/ex1.1/lake.pdf new file mode 100644 index 0000000..2808a4d Binary files /dev/null and b/lab3/exercise/ex1.1/lake.pdf differ diff --git a/lab3/exercise/ex1.1/lake.pha b/lab3/exercise/ex1.1/lake.pha new file mode 100644 index 0000000..0a5e7f5 --- /dev/null +++ b/lab3/exercise/ex1.1/lake.pha @@ -0,0 +1,40 @@ +r_in := 15; +r_out := 15.7; + +automaton lake +contr_var: x, t; + +synclabs: lakelab; +loc single: + while x >= 0 wait + { 0.7 * r_in - r_out <= x' <= r_in - r_out & t' == 1} + +initially: single & x == 25.7 & t == 0; +end + + + +// Compute the reachable set +// +region=lake.reachable; + +// +// Output to file + +region.print("lake_regions.txt", 0); + +region.project_to(t, x); +region.print("lake.txt", 2); + +// Safety verification + +forbidden = lake.{$ & x < 0}; +reach_set = lake.is_reachable(forbidden); +reach_set.intersection_assign(forbidden); + +echo "The intersection between the reachable set and the bad region is:"; +reach_set.is_empty; + + + + \ No newline at end of file diff --git a/lab3/exercise/ex1.1/lake.txt b/lab3/exercise/ex1.1/lake.txt new file mode 100644 index 0000000..93bf7a5 --- /dev/null +++ b/lab3/exercise/ex1.1/lake.txt @@ -0,0 +1,5 @@ +0 4.94230769230769162447814 +25.6999999999999992894573 0 +0 36.714285714285708195348 +0 4.94230769230769162447814 + diff --git a/lab3/exercise/ex1.1/lake_regions.txt b/lab3/exercise/ex1.1/lake_regions.txt new file mode 100644 index 0000000..257ea88 --- /dev/null +++ b/lab3/exercise/ex1.1/lake_regions.txt @@ -0,0 +1,3 @@ +region = lake.{ +single & 10*x + 7*t <= 257 & 10*x + 52*t >= 257 & x >= 0 +}; \ No newline at end of file diff --git a/lab3/exercise/ex1.2/lake2.pdf b/lab3/exercise/ex1.2/lake2.pdf new file mode 100644 index 0000000..f67a067 Binary files /dev/null and b/lab3/exercise/ex1.2/lake2.pdf differ diff --git a/lab3/exercise/ex1.2/lake2.pha b/lab3/exercise/ex1.2/lake2.pha new file mode 100644 index 0000000..0c58668 --- /dev/null +++ b/lab3/exercise/ex1.2/lake2.pha @@ -0,0 +1,47 @@ +r_in_r := 30; +r_in_d := 10; +r_out := 15.7; + +automaton lake +contr_var: x, t, c; + +synclabs: lakelab; +loc dry: + while x >= 0 & c <= 0.75 wait + { 0.7 * r_in_d - r_out <= x' <= r_in_d - r_out & t' == 1 & c' == 1} + when (c >= 0.75) sync lakelab goto rain; + +loc rain: + while x >= 0 & c <= 1 wait + { 0.7 * r_in_r - r_out <= x' <= r_in_r - r_out & t' == 1 & c' == 1} + when (c >= 1) sync lakelab do {c' == 0 & t' == t & x' == x} goto dry; + +initially: dry & x == 25.7 & t == 0 & c == 0; +end + + + +// Compute the reachable set +// +region=lake.reachable; + +// +// Output to file + +region.print("lake2_regions.txt", 0); + +region.project_to(t, x); +region.print("lake2.txt", 2); + +// Safety verification + +forbidden = lake.{$ & x < 0}; +reach_set = lake.is_reachable(forbidden); +reach_set.intersection_assign(forbidden); + +echo "The intersection between the reachable set and the bad region is:"; +reach_set.is_empty; + + + + \ No newline at end of file diff --git a/lab3/exercise/ex1.2/lake2.txt b/lab3/exercise/ex1.2/lake2.txt new file mode 100644 index 0000000..24c2ad7 --- /dev/null +++ b/lab3/exercise/ex1.2/lake2.txt @@ -0,0 +1,404 @@ +0 31.152298850574709376815 +1.32499999999999995559108 31 +4 31 +0 31.7017543859649109094789 +0 31.152298850574709376815 + +0 30.152298850574709376815 +1.32499999999999995559108 30 +4.69999999999999928945726 30 +0.42499999999999998889777 30.75 +0 30.75 +0 30.152298850574709376815 + +0 29.152298850574709376815 +1.32499999999999995559108 29 +5.39999999999999946709295 29 +1.125 29.75 +0 29.75 +0 29.152298850574709376815 + +0 28.152298850574709376815 +1.32499999999999995559108 28 +6.09999999999999964472863 28 +1.82499999999999995559108 28.75 +0 28.75 +0 28.152298850574709376815 + +19.1749999999999971578291 0.75 +25.6999999999999992894573 0 +21.4249999999999971578291 0.75 +19.1749999999999971578291 0.75 + +0 27.152298850574709376815 +1.32499999999999995559108 27 +6.79999999999999982236432 27 +2.52499999999999991118216 27.75 +0 27.75 +0 27.152298850574709376815 + +0 26.152298850574709376815 +1.32499999999999995559108 26 +7.5 26 +3.22499999999999964472863 26.75 +0 26.75 +0 26.152298850574709376815 + +0 25.152298850574709376815 +1.32499999999999995559108 25 +8.19999999999999928945726 25 +3.92499999999999982236432 25.75 +0 25.75 +0 25.152298850574709376815 + +0 24.152298850574709376815 +1.32499999999999995559108 24 +8.89999999999999857891453 24 +4.625 24.75 +0 24.75 +0 24.152298850574709376815 + +0 23.152298850574709376815 +1.32499999999999995559108 23 +9.59999999999999964472863 23 +5.32499999999999928945726 23.75 +0 23.75 +0 23.152298850574709376815 + +0 22.152298850574709376815 +1.32499999999999995559108 22 +10.2999999999999989341859 22 +6.02499999999999946709295 22.75 +0 22.75 +0 22.152298850574709376815 + +0 21.152298850574709376815 +1.32499999999999995559108 21 +11 21 +6.72499999999999964472863 21.75 +0 21.75 +0 21.152298850574709376815 + +13.9749999999999996447286 1.75 +20.5 1 +25 1 +20.7249999999999978683718 1.75 +13.9749999999999996447286 1.75 + +0 20.152298850574709376815 +1.32499999999999995559108 20 +11.6999999999999992894573 20 +7.42499999999999982236432 20.75 +0 20.75 +0 20.152298850574709376815 + +0 19.152298850574709376815 +1.32499999999999995559108 19 +12.3999999999999985789145 19 +8.125 19.75 +0 19.75 +0 19.152298850574709376815 + +0 18.152298850574709376815 +1.32499999999999995559108 18 +13.0999999999999996447286 18 +8.82499999999999928945726 18.75 +0 18.75 +0 18.152298850574709376815 + +0 17.152298850574709376815 +1.32499999999999995559108 17 +13.7999999999999989341859 17 +9.52499999999999857891453 17.75 +0 17.75 +0 17.152298850574709376815 + +0 16.152298850574709376815 +1.32499999999999995559108 16 +14.5 16 +10.2249999999999996447286 16.75 +0 16.75 +0 16.152298850574709376815 + +0 15.1522988505747111531718 +1.32499999999999995559108 15 +15.1999999999999992894573 15 +10.9249999999999989341859 15.75 +0 15.75 +0 15.1522988505747111531718 + +8.77499999999999857891453 2.75 +15.2999999999999989341859 2 +24.2999999999999971578291 2 +20.0249999999999985789145 2.75 +8.77499999999999857891453 2.75 + +0 14.1522988505747111531718 +1.32499999999999995559108 14 +15.8999999999999985789145 14 +11.625 14.75 +0 14.75 +0 14.1522988505747111531718 + +0 13.1522988505747111531718 +1.32499999999999995559108 13 +16.5999999999999978683718 13 +12.3249999999999992894573 13.75 +0 13.75 +0 13.1522988505747111531718 + +0 12.1522988505747111531718 +1.32499999999999995559108 12 +17.2999999999999971578291 12 +13.0249999999999985789145 12.75 +0 12.75 +0 12.1522988505747111531718 + +0 11.1522988505747111531718 +1.32499999999999995559108 11 +18 11 +13.7249999999999996447286 11.75 +0 11.75 +0 11.1522988505747111531718 + +0 10.1522988505747111531718 +1.32499999999999995559108 10 +18.6999999999999992894573 10 +14.4249999999999989341859 10.75 +0 10.75 +0 10.1522988505747111531718 + +0 9.15229885057471115317185 +1.32499999999999995559108 9 +19.3999999999999985789145 9 +15.125 9.75 +0 9.75 +0 9.15229885057471115317185 + +3.57499999999999973354647 3.75 +10.0999999999999996447286 3 +23.5999999999999978683718 3 +19.3249999999999992894573 3.75 +3.57499999999999973354647 3.75 + +0 8.15229885057471115317185 +1.32499999999999995559108 8 +20.0999999999999978683718 8 +15.8249999999999992894573 8.75 +0 8.75 +0 8.15229885057471115317185 + +0 7.15229885057471204135027 +1.32499999999999995559108 7 +20.7999999999999971578291 7 +16.5249999999999985789145 7.75 +0 7.75 +0 7.15229885057471204135027 + +0 6.15229885057471204135027 +1.32499999999999995559108 6 +21.5 6 +17.2249999999999978683718 6.75 +0 6.75 +0 6.15229885057471204135027 + +0 5.15229885057471204135027 +1.32499999999999995559108 5 +22.1999999999999992894573 5 +17.9249999999999971578291 5.75 +0 5.75 +0 5.15229885057471204135027 + +0 4.56321839080459756843311 +4.89999999999999946709295 4 +22.8999999999999985789145 4 +18.625 4.75 +0 4.75 +0 4.56321839080459756843311 + +0 30.75 +0.42499999999999998889777 30.75 +4 31 +1.32499999999999995559108 31 +0 30.75 + +0 29.75 +1.125 29.75 +4.69999999999999928945726 30 +1.32499999999999995559108 30 +0 29.75 + +0 28.75 +1.82499999999999995559108 28.75 +5.39999999999999946709295 29 +1.32499999999999995559108 29 +0 28.75 + +20.5 1 +19.1749999999999971578291 0.75 +21.4249999999999971578291 0.75 +25 1 +20.5 1 + +0 27.75 +2.52499999999999991118216 27.75 +6.09999999999999964472863 28 +1.32499999999999995559108 28 +0 27.75 + +0 26.75 +3.22499999999999964472863 26.75 +6.79999999999999982236432 27 +1.32499999999999995559108 27 +0 26.75 + +0 25.75 +3.92499999999999982236432 25.75 +7.5 26 +1.32499999999999995559108 26 +0 25.75 + +0 24.75 +4.625 24.75 +8.19999999999999928945726 25 +1.32499999999999995559108 25 +0 24.75 + +0 23.75 +5.32499999999999928945726 23.75 +8.89999999999999857891453 24 +1.32499999999999995559108 24 +0 23.75 + +0 22.75 +6.02499999999999946709295 22.75 +9.59999999999999964472863 23 +1.32499999999999995559108 23 +0 22.75 + +0 21.75 +6.72499999999999964472863 21.75 +10.2999999999999989341859 22 +1.32499999999999995559108 22 +0 21.75 + +15.2999999999999989341859 2 +13.9749999999999996447286 1.75 +20.7249999999999978683718 1.75 +24.2999999999999971578291 2 +15.2999999999999989341859 2 + +0 20.75 +7.42499999999999982236432 20.75 +11 21 +1.32499999999999995559108 21 +0 20.75 + +0 19.75 +8.125 19.75 +11.6999999999999992894573 20 +1.32499999999999995559108 20 +0 19.75 + +0 18.75 +8.82499999999999928945726 18.75 +12.3999999999999985789145 19 +1.32499999999999995559108 19 +0 18.75 + +0 17.75 +9.52499999999999857891453 17.75 +13.0999999999999996447286 18 +1.32499999999999995559108 18 +0 17.75 + +0 16.75 +10.2249999999999996447286 16.75 +13.7999999999999989341859 17 +1.32499999999999995559108 17 +0 16.75 + +0 15.75 +10.9249999999999989341859 15.75 +14.5 16 +1.32499999999999995559108 16 +0 15.75 + +10.0999999999999996447286 3 +8.77499999999999857891453 2.75 +20.0249999999999985789145 2.75 +23.5999999999999978683718 3 +10.0999999999999996447286 3 + +0 14.75 +11.625 14.75 +15.1999999999999992894573 15 +1.32499999999999995559108 15 +0 14.75 + +0 13.75 +12.3249999999999992894573 13.75 +15.8999999999999985789145 14 +1.32499999999999995559108 14 +0 13.75 + +0 12.75 +13.0249999999999985789145 12.75 +16.5999999999999978683718 13 +1.32499999999999995559108 13 +0 12.75 + +0 11.75 +13.7249999999999996447286 11.75 +17.2999999999999971578291 12 +1.32499999999999995559108 12 +0 11.75 + +0 10.75 +14.4249999999999989341859 10.75 +18 11 +1.32499999999999995559108 11 +0 10.75 + +0 9.75 +15.125 9.75 +18.6999999999999992894573 10 +1.32499999999999995559108 10 +0 9.75 + +4.89999999999999946709295 4 +3.57499999999999973354647 3.75 +19.3249999999999992894573 3.75 +22.8999999999999985789145 4 +4.89999999999999946709295 4 + +0 8.75 +15.8249999999999992894573 8.75 +19.3999999999999985789145 9 +1.32499999999999995559108 9 +0 8.75 + +0 7.75 +16.5249999999999985789145 7.75 +20.0999999999999978683718 8 +1.32499999999999995559108 8 +0 7.75 + +0 6.75 +17.2249999999999978683718 6.75 +20.7999999999999971578291 7 +1.32499999999999995559108 7 +0 6.75 + +0 5.75 +17.9249999999999971578291 5.75 +21.5 6 +1.32499999999999995559108 6 +0 5.75 + +0 4.75 +18.625 4.75 +22.1999999999999992894573 5 +1.32499999999999995559108 5 +0 4.75 + diff --git a/lab3/exercise/ex1.2/lake2_regions.txt b/lab3/exercise/ex1.2/lake2_regions.txt new file mode 100644 index 0000000..9a15da5 --- /dev/null +++ b/lab3/exercise/ex1.2/lake2_regions.txt @@ -0,0 +1,4 @@ +region = lake.{ +dry & (t == c + 31 & 40*x + 348*t >= 10841 & t >= 31 & 10*x + 57*t <= 1807 & x >= 0 | t == c + 30 & 40*x + 348*t >= 10493 & t >= 30 & 10*x + 57*t <= 1757 & x >= 0 & 4*t <= 123 | t == c + 29 & 40*x + 348*t >= 10145 & t >= 29 & 10*x + 57*t <= 1707 & x >= 0 & 4*t <= 119 | t == c + 28 & 40*x + 348*t >= 9797 & t >= 28 & 10*x + 57*t <= 1657 & x >= 0 & 4*t <= 115 | t == c & 10*x + 57*t <= 257 & 10*x + 87*t >= 257 & 4*t <= 3 | t == c + 27 & 40*x + 348*t >= 9449 & t >= 27 & 10*x + 57*t <= 1607 & x >= 0 & 4*t <= 111 | t == c + 26 & 40*x + 348*t >= 9101 & t >= 26 & 10*x + 57*t <= 1557 & x >= 0 & 4*t <= 107 | t == c + 25 & 40*x + 348*t >= 8753 & t >= 25 & 10*x + 57*t <= 1507 & x >= 0 & 4*t <= 103 | t == c + 24 & 40*x + 348*t >= 8405 & t >= 24 & 10*x + 57*t <= 1457 & x >= 0 & 4*t <= 99 | t == c + 23 & 40*x + 348*t >= 8057 & t >= 23 & 10*x + 57*t <= 1407 & x >= 0 & 4*t <= 95 | t == c + 22 & 40*x + 348*t >= 7709 & t >= 22 & 10*x + 57*t <= 1357 & x >= 0 & 4*t <= 91 | t == c + 21 & 40*x + 348*t >= 7361 & t >= 21 & 10*x + 57*t <= 1307 & x >= 0 & 4*t <= 87 | t == c + 1 & 10*x + 87*t >= 292 & t >= 1 & 10*x + 57*t <= 307 & 4*t <= 7 | t == c + 20 & 40*x + 348*t >= 7013 & t >= 20 & 10*x + 57*t <= 1257 & x >= 0 & 4*t <= 83 | t == c + 19 & 40*x + 348*t >= 6665 & t >= 19 & 10*x + 57*t <= 1207 & x >= 0 & 4*t <= 79 | t == c + 18 & 40*x + 348*t >= 6317 & t >= 18 & 10*x + 57*t <= 1157 & x >= 0 & 4*t <= 75 | t == c + 17 & 40*x + 348*t >= 5969 & t >= 17 & 10*x + 57*t <= 1107 & x >= 0 & 4*t <= 71 | t == c + 16 & 40*x + 348*t >= 5621 & t >= 16 & 10*x + 57*t <= 1057 & x >= 0 & 4*t <= 67 | t == c + 15 & 40*x + 348*t >= 5273 & t >= 15 & 10*x + 57*t <= 1007 & x >= 0 & 4*t <= 63 | t == c + 2 & 10*x + 87*t >= 327 & t >= 2 & 10*x + 57*t <= 357 & 4*t <= 11 | t == c + 14 & 40*x + 348*t >= 4925 & t >= 14 & 10*x + 57*t <= 957 & x >= 0 & 4*t <= 59 | t == c + 13 & 40*x + 348*t >= 4577 & t >= 13 & 10*x + 57*t <= 907 & x >= 0 & 4*t <= 55 | t == c + 12 & 40*x + 348*t >= 4229 & t >= 12 & 10*x + 57*t <= 857 & x >= 0 & 4*t <= 51 | t == c + 11 & 40*x + 348*t >= 3881 & t >= 11 & 10*x + 57*t <= 807 & x >= 0 & 4*t <= 47 | t == c + 10 & 40*x + 348*t >= 3533 & t >= 10 & 10*x + 57*t <= 757 & x >= 0 & 4*t <= 43 | t == c + 9 & 40*x + 348*t >= 3185 & t >= 9 & 10*x + 57*t <= 707 & x >= 0 & 4*t <= 39 | t == c + 3 & 10*x + 87*t >= 362 & t >= 3 & 10*x + 57*t <= 407 & 4*t <= 15 | t == c + 8 & 40*x + 348*t >= 2837 & t >= 8 & 10*x + 57*t <= 657 & x >= 0 & 4*t <= 35 | t == c + 7 & 40*x + 348*t >= 2489 & t >= 7 & 10*x + 57*t <= 607 & x >= 0 & 4*t <= 31 | t == c + 6 & 40*x + 348*t >= 2141 & t >= 6 & 10*x + 57*t <= 557 & x >= 0 & 4*t <= 27 | t == c + 5 & 40*x + 348*t >= 1793 & t >= 5 & 10*x + 57*t <= 507 & x >= 0 & 4*t <= 23 | t == c + 4 & 10*x + 87*t >= 397 & t >= 4 & 10*x + 57*t <= 457 & x >= 0 & 4*t <= 19), +rain & (t == c + 30 & 40*x >= 212*t - 6519 & 4*t >= 123 & 143*t >= 10*x + 4393 & t <= 31 | t == c + 29 & 40*x >= 212*t - 6307 & 4*t >= 119 & 143*t >= 10*x + 4243 & t <= 30 | t == c + 28 & 40*x >= 212*t - 6095 & 4*t >= 115 & 143*t >= 10*x + 4093 & t <= 29 | t == c & 10*x >= 53*t + 152 & 4*t >= 3 & 143*t >= 10*x - 107 & t <= 1 | t == c + 27 & 40*x >= 212*t - 5883 & 4*t >= 111 & 143*t >= 10*x + 3943 & t <= 28 | t == c + 26 & 40*x >= 212*t - 5671 & 4*t >= 107 & 143*t >= 10*x + 3793 & t <= 27 | t == c + 25 & 40*x >= 212*t - 5459 & 4*t >= 103 & 143*t >= 10*x + 3643 & t <= 26 | t == c + 24 & 40*x >= 212*t - 5247 & 4*t >= 99 & 143*t >= 10*x + 3493 & t <= 25 | t == c + 23 & 40*x >= 212*t - 5035 & 4*t >= 95 & 143*t >= 10*x + 3343 & t <= 24 | t == c + 22 & 40*x >= 212*t - 4823 & 4*t >= 91 & 143*t >= 10*x + 3193 & t <= 23 | t == c + 21 & 40*x >= 212*t - 4611 & 4*t >= 87 & 143*t >= 10*x + 3043 & t <= 22 | t == c + 1 & 10*x >= 53*t + 47 & 4*t >= 7 & 143*t >= 10*x + 43 & t <= 2 | t == c + 20 & 40*x >= 212*t - 4399 & 4*t >= 83 & 143*t >= 10*x + 2893 & t <= 21 | t == c + 19 & 40*x >= 212*t - 4187 & 4*t >= 79 & 143*t >= 10*x + 2743 & t <= 20 | t == c + 18 & 40*x >= 212*t - 3975 & 4*t >= 75 & 143*t >= 10*x + 2593 & t <= 19 | t == c + 17 & 40*x >= 212*t - 3763 & 4*t >= 71 & 143*t >= 10*x + 2443 & t <= 18 | t == c + 16 & 40*x >= 212*t - 3551 & 4*t >= 67 & 143*t >= 10*x + 2293 & t <= 17 | t == c + 15 & 40*x >= 212*t - 3339 & 4*t >= 63 & 143*t >= 10*x + 2143 & t <= 16 | t == c + 2 & 10*x >= 53*t - 58 & 4*t >= 11 & 143*t >= 10*x + 193 & t <= 3 | t == c + 14 & 40*x >= 212*t - 3127 & 4*t >= 59 & 143*t >= 10*x + 1993 & t <= 15 | t == c + 13 & 40*x >= 212*t - 2915 & 4*t >= 55 & 143*t >= 10*x + 1843 & t <= 14 | t == c + 12 & 40*x >= 212*t - 2703 & 4*t >= 51 & 143*t >= 10*x + 1693 & t <= 13 | t == c + 11 & 40*x >= 212*t - 2491 & 4*t >= 47 & 143*t >= 10*x + 1543 & t <= 12 | t == c + 10 & 40*x >= 212*t - 2279 & 4*t >= 43 & 143*t >= 10*x + 1393 & t <= 11 | t == c + 9 & 40*x >= 212*t - 2067 & 4*t >= 39 & 143*t >= 10*x + 1243 & t <= 10 | t == c + 3 & 10*x >= 53*t - 163 & 4*t >= 15 & 143*t >= 10*x + 343 & t <= 4 | t == c + 8 & 40*x >= 212*t - 1855 & 4*t >= 35 & 143*t >= 10*x + 1093 & t <= 9 | t == c + 7 & 40*x >= 212*t - 1643 & 4*t >= 31 & 143*t >= 10*x + 943 & t <= 8 | t == c + 6 & 40*x >= 212*t - 1431 & 4*t >= 27 & 143*t >= 10*x + 793 & t <= 7 | t == c + 5 & 40*x >= 212*t - 1219 & 4*t >= 23 & 143*t >= 10*x + 643 & t <= 6 | t == c + 4 & 40*x >= 212*t - 1007 & 4*t >= 19 & 143*t >= 10*x + 493 & t <= 5) +}; \ No newline at end of file diff --git a/lab3/phaver b/lab3/phaver new file mode 100755 index 0000000..563eadc Binary files /dev/null and b/lab3/phaver differ diff --git a/lab3/phaverplot.gp b/lab3/phaverplot.gp new file mode 100644 index 0000000..f264cd2 --- /dev/null +++ b/lab3/phaverplot.gp @@ -0,0 +1,2 @@ +set offsets graph 0.1, 0.1, 0.1, 0.1 +plot ARG1 using 1:2 with filledcurves \ No newline at end of file