Skip to content
Permalink
Branch: master
Find file Copy path
Find file Copy path
Fetching contributors…
Cannot retrieve contributors at this time
4703 lines (4305 sloc) 220 KB
Theorem "Theorem 1: Static safety".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (v^2 / (2*b())). /* The straight-line stopping distance from brake start to full stop. */
R accelComp(R v) = ((A()/b() + 1) * (A()/2 * ep()^2 + ep()*v))./* Straight-line distance to compensate acceleration */
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)). /* Separation that allows accelerating on a new curve */
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
t := 0;
}
/* dynamics */
{
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
t' = 1 & t <= ep & v >= 0
}@invariant(t>=0, isWellformedDir(),
(v'=-b() -> v = old(v) - b()*t),
(v'=-b() -> (-t * (old(v) - b()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) - b()/2*t))),
(v'=-b() -> (-t * (old(v) - b()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) - b()/2*t))),
(v'=0 -> v = old(v)),
(v'=0 -> x = old(x)),
(v'=0 -> y = old(y)),
(v'=A() -> v = old(v) + A()*t),
(v'=A() -> (-t * (old(v) + A()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) + A()/2*t))),
(v'=A() -> (-t * (old(v) + A()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) + A()/2*t)))
)
}
}*@invariant(loopinv())
](x - xo)^2 + (y - yo)^2 > 0
End.
Tactic "Proof Theorem 1: Static safety".
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1)
);
tactic dib as (
diall;
diffInvariant({`v = old(v) - b()*t`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= x - old(x) & x - old(x) <= t * (v + b()/2*t)`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= y - old(y) & y - old(y) <= t * (v + b()/2*t)`}, 1)
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
diffInvariant({`v = old(v) + A()*t`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= x - old(x) & x - old(x) <= t * (v - A()/2*t)`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= y - old(y) & y - old(y) <= t * (v - A()/2*t)`}, 1)
);
tactic dw as (andL('L)*; dW(1));
tactic xAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(x_0-xo)>v_0^2/(2*b())+(A()/b()+1)*(A()/2*t^2+t*v_0)`}, 'L=={`abs(x_0-xo)>admissibleSeparation(v_0)`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(y_0-yo)>v_0^2/(2*b())+(A()/b()+1)*(A()/2*t^2+t*v_0)`}, 'L=={`abs(y_0-yo)>admissibleSeparation(v_0)`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`abs(x-xo_0)>stopDist(v)|abs(y-yo_0)>stopDist(v)`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
Tactic "Proof Theorem 1: Static safety from annotations".
master
End.
End.
ArchiveEntry "Corollary 1.1: Velocity-controlled passive safety".
Functions.
R ep(). /* time limit for control decisions */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (0).
R accelComp(R v) = (ep()*(v+V())).
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
ep() > 0 /* Controller reaction time */
& V() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ v := 0; w := 0; }
++
/* or choose a new safe curve */
{ v := *; ?0<=v;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
t := 0;
}
/* dynamics */
{
{ x' = v * dx, y' = v * dy, /* move */
dx' = -w * dy, dy' = w * dx, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}@invariant(t>=0, isWellformedDir(),
(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V()),
(-t*V() <= yo - old(yo) & yo - old(yo) <= t*V()),
(x'=0*dx -> x = old(x)),
(x'=0*dx -> y = old(y)),
(x'=v*dx -> -t * v <= x - old(x) & x - old(x) <= t * v),
(x'=v*dx -> -t * v <= y - old(y) & y - old(y) <= t * v)
)
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Corollary 1: Velocity-controlled passive safety".
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
diffInvariant({`-t*V() <= xo - old(xo) & xo - old(xo) <= t*V()`}, 1);
diffInvariant({`-t*V() <= yo - old(yo) & yo - old(yo) <= t*V()`}, 1)
);
tactic di0 as (
diall;
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
diffInvariant({`-t * v <= x - old(x) & x - old(x) <= t * v`}, 1);
diffInvariant({`-t * v <= y - old(y) & y - old(y) <= t * v`}, 1)
);
tactic dw as (andL('L)*; dW(1));
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Stopped branch`}); di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`v_0>0 -> abs(x-xo_0)>stopDist(v_0) | abs(y-yo_0)>stopDist(v_0)`});
dia; dw; prop; doall(smartQE); print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Corollary 1.2: Static safety with margin for imperfect trajectories".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R Ud(). /* direction uncertainty */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = ((1+Ud()) * v^2 / (2*b())). /* The straight-line stopping distance from brake start to full stop. */
R accelComp(R v) = ((1+Ud()) * (A()/b() + 1) * (A()/2 * ep()^2 + ep()*v)). /* Straight-line distance to compensate acceleration */
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)). /* Separation that allows accelerating on a new curve */
B isWellformedDir() <-> (1-Ud() <= dx^2+dy^2 & dx^2 + dy^2 <= 1+Ud()). /* The orientation of the robot is approximately a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& 0<=Ud() & Ud() <= 1
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
t := 0;
}
/* dynamics */
{
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
t' = 1 & t <= ep & v >= 0
}@invariant(t>=0, isWellformedDir(),
(v'=-b() -> v <= old(v) - b()*t),
(v'=-b() -> (-t * (old(v) - b()/2*t) * (1+Ud()) <= x - old(x) & x - old(x) <= t * (old(v) - b()/2*t) * (1+Ud()))),
(v'=-b() -> (-t * (old(v) - b()/2*t) * (1+Ud()) <= y - old(y) & y - old(y) <= t * (old(v) - b()/2*t) * (1+Ud()))),
(v'=0 -> v = old(v)),
(v'=0 -> x = old(x)),
(v'=0 -> y = old(y)),
(v'=A() -> v <= old(v) + A()*t),
(v'=A() -> (-t * (old(v) + A()/2*t) * (1+Ud()) <= x - old(x) & x - old(x) <= t * (old(v) + A()/2*t) * (1+Ud()))),
(v'=A() -> (-t * (old(v) + A()/2*t) * (1+Ud()) <= y - old(y) & y - old(y) <= t * (old(v) + A()/2*t) * (1+Ud())))
)
}
}*@invariant(loopinv())
](x - xo)^2 + (y - yo)^2 > 0
End.
Tactic "Proof Theorem 1: Static safety".
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1)
);
tactic diHide as (
hideL('L~={`abs(x-xo)>stopDist(v)|abs(y-yo)>stopDist(v)`});
hideL('L~={`1-Ud()<=dx^2+dy^2`});
hideL('L~={`dx^2+dy^2<=1+Ud()`})
);
tactic dib as (
diall;
dC({`v <= old(v) - b()*t`}, 1); <(nil, diHide; dI(1));
dC({`(-t * (old(v) - b()/2*t) * (1+Ud()) <= x - old(x) & x - old(x) <= t * (old(v) - b()/2*t) * (1+Ud()))
& (-t * (old(v) - b()/2*t) * (1+Ud()) <= y - old(y) & y - old(y) <= t * (old(v) - b()/2*t) * (1+Ud()))`}, 1); <(nil, diHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
dC({`v = old(v)`}, 1); <(nil, diHide; dI(1));
dC({`x = old(x)`}, 1); <(nil, diHide; dI(1));
dC({`y = old(y)`}, 1); <(nil, diHide; dI(1))
);
tactic diaHide as (
hideL('L~={`abs(x-xo)>admissibleSeparation(v)|abs(y-yo)>admissibleSeparation(v)`});
hideL('L~={`1-Ud()<=dx^2+dy^2`});
hideL('L~={`dx^2+dy^2<=1+Ud()`})
);
tactic dia as (
diall;
dC({`v <= old(v) + A()*t`}, 1); <(nil, diaHide; dI(1));
dC({`(-t * (old(v) + A()/2*t) * (1+Ud()) <= x - old(x) & x - old(x) <= t * (old(v) + A()/2*t) * (1+Ud()))
& (-t * (old(v) + A()/2*t) * (1+Ud()) <= y - old(y) & y - old(y) <= t * (old(v) + A()/2*t) * (1+Ud()))`}, 1); <(nil, diaHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
tactic qeHide as (
hideL('L~={`1-Ud()<=dx^2+dy^2`})*;
hideL('L~={`dx^2+dy^2<=1+Ud()`})*
);
tactic xAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(x_0-xo)>(1+Ud())*(v_0^2/(2*b())+(A()/b()+1)*(A()/2*t^2+t*v_0))`}, 'L=={`abs(x_0-xo)>admissibleSeparation(v_0)`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
qeHide;
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(y_0-yo)>(1+Ud())*(v_0^2/(2*b())+(A()/b()+1)*(A()/2*t^2+t*v_0))`}, 'L=={`abs(y_0-yo)>admissibleSeparation(v_0)`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
qeHide;
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(qeHide; smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(qeHide; smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`abs(x-xo_0)>stopDist(v)|abs(y-yo_0)>stopDist(v)`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Corollary 1.3: Static safety with margin for imperfect trajectories (no division)".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R Ud(). /* direction uncertainty */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = ((1+Ud()) * v^2). /* The straight-line stopping distance from brake start to full stop. */
R accelComp(R v, R t) = ((1+Ud()) * (A() + b()) * (A() * t^2 + 2*t*v)). /* Straight-line distance to compensate acceleration */
R admissibleSeparation(R v, R t) = (stopDist(v) + accelComp(v,t)). /* Separation that allows accelerating on a new curve */
B isWellformedDir() <-> (1-Ud() <= dx^2+dy^2 & dx^2 + dy^2 <= 1+Ud()). /* The orientation of the robot is approximately a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& 0<=Ud() & Ud() <= 1
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0 & a = 0 & w = 0 & r = 1 & t = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (2*b()*abs(x-xo) > stopDist(v) | 2*b()*abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
{
/* brake on current curve or remain stopped */
{ a := -b(); }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? 2*b()*abs(x-xo) > admissibleSeparation(v,ep)
| 2*b()*abs(y-yo) > admissibleSeparation(v,ep);
}
};
t := 0;
}
/* dynamics */
{
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
t' = 1 & t <= ep & v >= 0
}@invariant(t>=0, isWellformedDir(),
(v'=-b() -> v <= old(v) - b()*(t-old(t))),
(v'=-b() -> (-(t-old(t)) * (2*old(v) - b()*(t-old(t))) * (1+Ud()) <= 2*(x - old(x)) & 2*(x - old(x)) <= (t-old(t)) * (2*old(v) - b()*(t-old(t))) * (1+Ud()))),
(v'=-b() -> (-(t-old(t)) * (2*old(v) - b()*(t-old(t))) * (1+Ud()) <= 2*(y - old(y)) & 2*(y - old(y)) <= (t-old(t)) * (2*old(v) - b()*(t-old(t))) * (1+Ud()))),
(v'=0 -> v = old(v)),
(v'=0 -> x = old(x)),
(v'=0 -> y = old(y)),
(v'=0 -> w = old(w)), /* may not be necessary if we remove w=0 from throughout inv */
(v'=A() -> v <= old(v) + A()*(t-old(t))),
(v'=A() -> (-(t-old(t)) * (2*old(v) + A()*(t-old(t))) * (1+Ud()) <= 2*(x - old(x)) & 2*(x - old(x)) <= (t-old(t)) * (2*old(v) + A()*(t-old(t))) * (1+Ud()))),
(v'=A() -> (-(t-old(t)) * (2*old(v) + A()*(t-old(t))) * (1+Ud()) <= 2*(y - old(y)) & 2*(y - old(y)) <= (t-old(t)) * (2*old(v) + A()*(t-old(t))) * (1+Ud())))
)
}
}*@invariant(loopinv())
](x - xo)^2 + (y - yo)^2 > 0
End.
Tactic "Proof Theorem 1: Static safety".
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1)
);
tactic diHide as (
hideL('L~={`2*b()*abs(x-xo)>stopDist(v)|2*b()*abs(y-yo)>stopDist(v)`});
hideL('L~={`1-Ud()<=dx^2+dy^2`});
hideL('L~={`dx^2+dy^2<=1+Ud()`})
);
tactic dib as (
diall;
dC({`v <= old(v) - b()*t`}, 1); <(nil, diHide; dI(1));
dC({`(-t * (2*old(v) - b()*t) * (1+Ud()) <= 2*(x - old(x)) & 2*(x - old(x)) <= t * (2*old(v) - b()*t) * (1+Ud()))
& (-t * (2*old(v) - b()*t) * (1+Ud()) <= 2*(y - old(y)) & 2*(y - old(y)) <= t * (2*old(v) - b()*t) * (1+Ud()))`}, 1); <(nil, diHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic diaHide as (
hideL('L~={`2*b()*abs(x-xo)>admissibleSeparation(v)|2*b()*abs(y-yo)>admissibleSeparation(v)`});
hideL('L~={`1-Ud()<=dx^2+dy^2`});
hideL('L~={`dx^2+dy^2<=1+Ud()`});
hideL('L=={`r*w=v_0`}); hideL('L=={`-W()<=w`}); hideL('L=={`w<=W()`}); hideL('L=={`r!=0`})
);
tactic dia as (
diall;
dC({`v <= old(v) + A()*t`}, 1); <(nil, diaHide; dI(1));
dC({`(-t * (2*old(v) + A()*t) * (1+Ud()) <= 2*(x - old(x)) & 2*(x - old(x)) <= t * (2*old(v) + A()*t) * (1+Ud()))
& (-t * (2*old(v) + A()*t) * (1+Ud()) <= 2*(y - old(y)) & 2*(y - old(y)) <= t * (2*old(v) + A()*t) * (1+Ud()))`}, 1); <(nil, diaHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
tactic qeHide as (
hideL('L~={`1-Ud()<=dx^2+dy^2`})*;
hideL('L~={`dx^2+dy^2<=1+Ud()`})*
);
tactic xAccArith as (
andL('L)*;
hideR('R=={`2*b()*abs(y-yo)>stopDist(v)`});
hideL('L=={`1-Ud()<=dx^2+dy^2`});
hideL('L=={`dx^2+dy^2<=1+Ud()`});
hideL('L=={`1-Ud()<=dx_0^2+dy_0^2`});
hideL('L=={`dx_0^2+dy_0^2<=1+Ud()`});
hideL('L=={`-W()<=w_0`});
hideL('L=={`w_0<=W()`});
hideL('L=={`r!=0`});
hideL('L=={`r*w_0=v_0`});
print({`Transforming...`});
transform({`2*b()*abs(x_0-xo)>(1+Ud())*(v_0^2+(A()+b())*(A()*t^2+2*t*v_0))`}, 'L=={`2*b()*abs(x_0-xo)>admissibleSeparation(v_0,ep())`});
hideL('L=={`t_0=0`});
hideL('L=={`t<=ep()`});
hideL('L=={`ep()>0`});
print({`Transformed`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
hideR('R=={`2*b()*abs(x-xo)>stopDist(v)`});
hideL('L=={`1-Ud()<=dx^2+dy^2`});
hideL('L=={`dx^2+dy^2<=1+Ud()`});
hideL('L=={`1-Ud()<=dx_0^2+dy_0^2`});
hideL('L=={`dx_0^2+dy_0^2<=1+Ud()`});
hideL('L=={`-W()<=w_0`});
hideL('L=={`w_0<=W()`});
hideL('L=={`r!=0`});
hideL('L=={`r*w_0=v_0`});
print({`Transforming...`});
transform({`2*b()*abs(y_0-yo)>(1+Ud())*(v_0^2+(A()+b())*(A()*t^2+2*t*v_0))`}, 'L=={`2*b()*abs(y_0-yo)>admissibleSeparation(v_0,ep())`});
hideL('L=={`t_0=0`});
hideL('L=={`t<=ep()`});
hideL('L=={`ep()>0`});
print({`Transformed`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(qeHide; smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(qeHide; smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L=={`2*b()*abs(x-xo_0)>(1+Ud())*v^2|2*b()*abs(y-yo_0)>(1+Ud())*v^2`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
Tactic "Proof with throughout invariant".
implyR(1) ; throughout({`(v>=0&(1-Ud()<=dx^2+dy^2&dx^2+dy^2<=1+Ud())&(2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2))&t>=0&(a=-b()|v=0&a=0|a=A()&(2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)))`}, 1) ; <(
simplify(1) ; smartQE,
andL(-1) ; hideL(-7=={`t>=0&(a=-b()|v=0&a=0|a=A()&(2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)))`}) ; andL(-6) ; andL(-7) ; hideL(-7=={`1-Ud()<=dx^2+dy^2&dx^2+dy^2<=1+Ud()`}) ; QE,
chase(1) ; simplify(1) ; andR(1) ; <(
prop,
(allR(1) | implyR(1))* ; orR(1) ; andL(-1) ; andL(-9) ; hideL(-11=={`(1-Ud()<=dx^2+dy^2&dx^2+dy^2<=1+Ud())&(2*b()*abs(x-xo_0)>(1+Ud())*v^2|2*b()*abs(y-yo_0)>(1+Ud())*v^2)`}) ; hideL(-9=={`t>=0&(a=-b()|v=0&a=0|a=A()&(2*b()*abs(x-xo_0)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo_0)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)))`}) ; smartQE
),
andL('L)* ; orL(-5) ; <(
allL2R(-5) ; hideL(-5=={`a=-b()`}) ; dC({`t>=old(t)`}, 1) ; <(
dC({`1-Ud()<=dx^2+dy^2&dx^2+dy^2<=1+Ud()`}, 1) ; <(
dC({`v<=old(v)-b()*(t-old(t))`}, 1) ; <(
dC({`-(t-old(t))*(2*old(v)-b()*(t-old(t)))*(1+Ud())<=2*(x-old(x))&2*(x-old(x))<=(t-old(t))*(2*old(v)-b()*(t-old(t)))*(1+Ud())`}, 1) ; <(
dC({`-(t-old(t))*(2*old(v)-b()*(t-old(t)))*(1+Ud())<=2*(y-old(y))&2*(y-old(y))<=(t-old(t))*(2*old(v)-b()*(t-old(t)))*(1+Ud())`}, 1) ; <(
dW(1) ; simplify(1) ; implyR(1) ; andR(1) ; <(
andL('L)* ; orR(1) ; hideL(-22=={`t<=ep()`}) ; hideL(-21=={`dx^2+dy^2<=1+Ud()`}) ; hideL(-20=={`1-Ud()<=dx^2+dy^2`}) ; hideL(-11=={`ep()>0`}) ; hideL(-9=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-8=={`1-Ud()<=dx_0^2+dy_0^2`}) ; hideL(-7=={`A()>=0`}) ; hideL(-5=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-3=={`v_0>=0`}) ; hideL(-2=={`1-Ud()<=dx_0^2+dy_0^2`}) ; orL(-3) ; <(
hideR(2=={`2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; hideL(-8=={`2*(y-y_0)<=(t-t_0)*(2*v_0-b()*(t-t_0))*(1+Ud())`}) ; hideL(-7=={`-(t-t_0)*(2*v_0-b()*(t-t_0))*(1+Ud())<=2*(y-y_0)`}) ; smartQE,
hideR(1=={`2*b()*abs(x-xo)>(1+Ud())*v^2`}) ; hideL(-11=={`2*(x-x_0)<=(t-t_0)*(2*v_0-b()*(t-t_0))*(1+Ud())`}) ; hideL(-10=={`-(t-t_0)*(2*v_0-b()*(t-t_0))*(1+Ud())<=2*(x-x_0)`}) ; smartQE
),
QE
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
orL(-5) ; <(
andL(-5) ; allL2R(-15=={`a=0`}) ; hideL(-15=={`a=0`}) ; dC({`t>=old(t)`}, 1) ; <(
dC({`1-Ud()<=dx^2+dy^2&dx^2+dy^2<=1+Ud()`}, 1) ; <(
dC({`v=old(v)`}, 1) ; <(
dC({`x=old(x)`}, 1) ; <(
dC({`y=old(y)`}, 1) ; <(
dW(1) ; implyR(1) ; andR(1) ; <(
andL('L)* ; allL2R(-17=={`v=v_0`}) ; hideL(-17=={`v=v_0`}) ; allL2R(-16=={`x=x_0`}) ; hideL(-16=={`x=x_0`}) ; allL2R(-15=={`y=y_0`}) ; hideL(-15=={`y=y_0`}) ; simplify(1) ; closeTrue,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; hideR(3=={`0=A()&(2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v))`}) ; hideR(1=={`0=-b()`}) ; simplify(1) ; QE
)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dI(1)
),
andL(-5) ; allL2R(-14=={`a=A()`}) ; hideL(-14=={`a=A()`}) ; hideL(-6=={`2*b()*abs(x-xo)>(1+Ud())*v^2|2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; dC({`t>=old(t)`}, 1) ; <(
dC({`1-Ud()<=dx^2+dy^2&dx^2+dy^2<=1+Ud()`}, 1) ; <(
dC({`v<=old(v)+A()*(t-old(t))`}, 1) ; <(
dC({`-(t-old(t))*(2*old(v)+A()*(t-old(t)))*(1+Ud())<=2*(x-old(x))&2*(x-old(x))<=(t-old(t))*(2*old(v)+A()*(t-old(t)))*(1+Ud())`}, 1) ; <(
dC({`-(t-old(t))*(2*old(v)+A()*(t-old(t)))*(1+Ud())<=2*(y-old(y))&2*(y-old(y))<=(t-old(t))*(2*old(v)+A()*(t-old(t)))*(1+Ud())`}, 1) ; <(
dW(1) ; implyR(1) ; andL('L)* ; andR(1) ; <(
andR(1) ; <(
hideL(-13=={`2*b()*abs(x_0-xo)>(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)|2*b()*abs(y_0-yo)>(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; QE,
andR(1) ; <(
prop,
orR(1) ; hideL(-21=={`dx^2+dy^2<=1+Ud()`}) ; hideL(-20=={`1-Ud()<=dx^2+dy^2`}) ; hideL(-8=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-7=={`1-Ud()<=dx_0^2+dy_0^2`}) ; hideL(-5=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-3=={`v_0>=0`}) ; hideL(-2=={`1-Ud()<=dx_0^2+dy_0^2`}) ; orL(-8) ; <(
hideL(-9=={`-(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())<=2*(y-y_0)`}) ; hideL(-9=={`2*(y-y_0)<=(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())`}) ; edit({`2*b()*abs(x_0-xo)>(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(t-t_0)^2+2*(t-t_0)*v_0)`}, -8) ; hideR(2=={`2*b()*abs(y-yo)>(1+Ud())*v^2`}) ; hideL(-13=={`t<=ep()`}) ; hideL(-5=={`ep()>0`}) ; smartQE,
hideR(1=={`2*b()*abs(x-xo)>(1+Ud())*v^2`}) ; hideL(-13=={`2*(x-x_0)<=(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())`}) ; hideL(-12=={`-(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())<=2*(x-x_0)`}) ; edit({`2*b()*abs(y_0-yo)>(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(t-t_0)^2+2*(t-t_0)*v_0)`}, -8) ; hideL(-13=={`t<=ep()`}) ; hideL(-5=={`ep()>0`}) ; smartQE
)
)
),
andR(1) ; <(
QE,
orR(1) ; orR(2) ; hideR(1=={`A()=-b()`}) ; hideR(1=={`v=0&A()=0`}) ; simplify(1) ; orR(1) ; orL(-13) ; <(
hideR(2=={`2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; hideL(-21=={`dx^2+dy^2<=1+Ud()`}) ; hideL(-20=={`1-Ud()<=dx^2+dy^2`}) ; hideL(-8=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-7=={`1-Ud()<=dx_0^2+dy_0^2`}) ; hideL(-5=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-3=={`v_0>=0`}) ; hideL(-2=={`1-Ud()<=dx_0^2+dy_0^2`}) ; hideL(-9=={`-(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())<=2*(y-y_0)`}) ; hideL(-9=={`2*(y-y_0)<=(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())`}) ; cut({`(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)+b()*(t-t_0)*(1+Ud())*(A()*(t-t_0)+2*v_0)<=(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; <(
edit({`(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)+b()*(t-t_0)*(1+Ud())*(A()*(t-t_0)+2*v_0)<=abbrv((1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0))`}, -15) ; edit({`abbrv((1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v))+b()*(t-t_0)*(1+Ud())*(A()*(t-t_0)+2*v_0)<=abbrv`}, -15) ; hideL(-16=={`abbrv=(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; hideL(-16=={`abbrv_0=(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; smartQE,
hideR(1=={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; hideL(-8=={`2*b()*abs(x_0-xo)>(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; QE
),
hideR(1=={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; hideL(-17=={`-(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())<=2*(x-x_0)`}) ; hideL(-17=={`2*(x-x_0)<=(t-t_0)*(2*v_0+A()*(t-t_0))*(1+Ud())`}) ; hideL(-19=={`dx^2+dy^2<=1+Ud()`}) ; hideL(-18=={`1-Ud()<=dx^2+dy^2`}) ; hideL(-8=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-7=={`1-Ud()<=dx_0^2+dy_0^2`}) ; hideL(-5=={`dx_0^2+dy_0^2<=1+Ud()`}) ; hideL(-3=={`v_0>=0`}) ; hideL(-2=={`1-Ud()<=dx_0^2+dy_0^2`}) ; cut({`(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)+b()*(t-t_0)*(1+Ud())*(A()*(t-t_0)+2*v_0)<=(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; <(
edit({`(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)+b()*(t-t_0)*(1+Ud())*(A()*(t-t_0)+2*v_0)<=abbrv((1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0))`}, -15) ; edit({`abbrv((1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v))+b()*(t-t_0)*(1+Ud())*(A()*(t-t_0)+2*v_0)<=abbrv`}, -15) ; hideL(-16=={`abbrv=(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; hideL(-16=={`abbrv_0=(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; smartQE,
hideR(1=={`2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; hideL(-8=={`2*b()*abs(y_0-yo)>(1+Ud())*v_0^2+(1+Ud())*(A()+b())*(A()*(ep()-t_0)^2+2*(ep()-t_0)*v_0)`}) ; QE
)
)
)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; dI(1)
),
hideL('L~={`2*b()*abs(x-xo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)|2*b()*abs(y-yo)>(1+Ud())*v^2+(1+Ud())*(A()+b())*(A()*(ep()-t)^2+2*(ep()-t)*v)`}) ; dI(1)
)
)
)
)
End.
End.
Theorem "Theorem 2: Passive safety".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (v^2 / (2*b()) + V()*v/b()).
R accelComp(R v) = ((A()/b() + 1) * (A()/2 * ep()^2 + ep()*(v+V))).
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
t := 0;
}
/* dynamics */
{
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}@invariant(t>=0, isWellformedDir(),
(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V()),
(-t*V() <= yo - old(yo) & yo - old(yo) <= t*V()),
(v'=-b() -> v = old(v) - b()*t),
(v'=-b() -> (-t * (old(v) - b()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) - b()/2*t))),
(v'=-b() -> (-t * (old(v) - b()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) - b()/2*t))),
(v'=0 -> v = old(v)),
(v'=0 -> x = old(x)),
(v'=0 -> y = old(y)),
(v'=A() -> v = old(v) + A()*t),
(v'=A() -> (-t * (old(v) + A()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) + A()/2*t))),
(v'=A() -> (-t * (old(v) + A()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) + A()/2*t)))
)
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 2: Passive safety".
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
diffInvariant({`-t*V() <= xo - old(xo) & xo - old(xo) <= t*V()`}, 1);
diffInvariant({`-t*V() <= yo - old(yo) & yo - old(yo) <= t*V()`}, 1)
);
tactic dib as (
diall;
diffInvariant({`v = old(v) - b()*t`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= x - old(x) & x - old(x) <= t * (v + b()/2*t)`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= y - old(y) & y - old(y) <= t * (v + b()/2*t)`}, 1)
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
diffInvariant({`v = old(v) + A()*t`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= x - old(x) & x - old(x) <= t * (v - A()/2*t)`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= y - old(y) & y - old(y) <= t * (v - A()/2*t)`}, 1)
);
tactic dw as (andL('L)*; dW(1));
tactic xAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(x_0-xo_0)>admissibleSeparation(v_0)`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(y_0-yo_0)>admissibleSeparation(v_0)`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`v>0 -> abs(x-xo_0)>stopDist(v) | abs(y-yo_0)>stopDist(v)`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
ArchiveEntry "Corollary 2: Velocity-controlled passive orientation safety".
Functions.
R ep(). /* time limit for control decisions */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R Gamma(). /* Sensor range in radian */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = ( 0 ).
R stopMargin(R v) = ( stopDist(v) ).
R accelComp(R v) = ( ep()*v ).
R accelMargin(R v) = ( accelComp(v) + ep()*V() ).
R admissibleSeparation(R v) = ( stopMargin(v) + accelMargin(v) ).
R admissibleTurnLength(R v) = ( stopDist(v) + accelComp(v) ).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B isVisible(R) <-> ((.)>0). /* Indicates whether or not the obstacle is visible for the robot at the decision. */
B bounds() <-> ( /* Bounds for global constants */
ep() > 0 /* Controller reaction time */
& V() >= 0
& Gamma() > 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& beta = 0
& r != 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& r != 0
& (v>0 -> ( (abs(x-xo) > stopMargin(v) | abs(y-yo) > stopMargin(v))
| (!isVisible(visDeg) & abs(beta) + stopDist(v)/abs(r) < Gamma() )) )
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
R beta. /* Angle that the robot traveled since it last chose a new curve */
R visDeg. /* Indicates the "degree" to which the obstacle is visible to the robot (input to isVisible) */
End.
Problem.
assumptions() -> [
{
{
/* obstacle control */
{
vxo := *;
vyo := *;
?vxo^2+vyo^2 <= V()^2;
}
/* robot control */
{
/* brake on current curve. If the velocity is zero this just means that the robot remains stopped */
{v := 0; w := 0;}
++ /* or choose a new safe curve */
{v := *;
beta := 0;
r :=*; ?r!=0;
/* measure obstacle position and whether or not it is visible to the robot */
xo := *; yo := *; visDeg := *;
?(isVisible(visDeg) ->
( abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v)) );
?admissibleTurnLength(v) < Gamma()*abs(r);
}
}
/* Reset the clocks */
t := 0;
/* Set w according to physics (rigid body motion) */
w :=*; ?w*r = v;
}
{x' = v * dx, y' = v * dy, dx' = -w * dy, dy' = w * dx, beta'=w,
xo' = vxo, yo' = vyo, t' = 1 & (t <= ep & v >= 0)}
}*
] (v > 0 -> ((x - xo)^2 + (y - yo)^2 > 0 | (!isVisible(visDeg) & (abs(beta) < Gamma()))) )
End.
Tactic "Proof Corollary 2: Velocity-controlled passive orientation safety".
tactic diHide as (
hideL('L~={`visDeg>0->abs(x-xo)>0+(ep()*v+ep()*V())|abs(y-yo)>0+(ep()*v+ep()*V())`})*;
hideL('L~={`v>0->(abs(x-xo_0)>0|abs(y-yo)>0)|!visDeg>0&abs(beta)+0/abs(r) < Gamma()`})*
);
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
dC({`(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V())
& (-t*V() <= yo - old(yo) & yo - old(yo) <= t*V())`}, 1); <(nil, diHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
diffInvariant({`beta = old(beta)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
diffInvariant({`beta = old(beta) + t*v/r`}, 1);
dC({`(-t * v <= x - old(x) & x - old(x) <= t * v)
& (-t * v <= y - old(y) & y - old(y) <= t * v)`}, 1); <(nil, diHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Stopped branch`}); di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`v_0>0->((abs(x-xo_0)>stopMargin(v_0)|abs(y-yo_0)>stopMargin(v_0))|!isVisible(visDeg_0)&abs(beta_0)+stopDist(v_0)/abs(r_0) < Gamma())`});
unfold;
dia; dw;
print({`Acceleration arithmetic`});
implyR(1) ; andL('L)* ; simplify(1); implyR(1) ; orR(1) ; orR(1) ;
implyL('L=={`isVisible(visDeg) -> ( abs(x_0-xo_0) > admissibleSeparation(v) | abs(y_0-yo_0) > admissibleSeparation(v))`}) ; <(
hideR('R=={`abs(x-xo)>stopMargin(v)`}) ; hideR('R=={`abs(y-yo)>stopMargin(v)`}) ; fullSimplify ; andR(1) ; doall(smartQE)
,
print({`Acc Distance`});
hideL('L=={`admissibleTurnLength(v) < Gamma()*abs(r)`}) ;
hideR('R=={`visDeg<=0 & abs(beta) + stopDist(v)/abs(r) < Gamma()`});
hideL('L=={`r_0!=0`});
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`dx^2+dy^2=1`});
hideL('L=={`Gamma()>0`});
hideL('L=={`beta_0=0`});
hideL('L=={`w*r=v`});
hideL('L=={`beta=beta_0+t*v/r`});
orL('L=={`abs(x_0-xo_0)>admissibleSeparation(v) | abs(y_0-yo_0)>admissibleSeparation(v)`}); <(
fullSimplify ; smartQE
,
fullSimplify ; smartQE
)
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 3: Passive Friendly Safety".
Functions.
R ep(). /* time limit for control decisions */
R tau(). /* time limit for obstacle reaction */
R b(). /* minimum braking capability of the robot */
R bo(). /* obstacle brakes */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R abs(R). /* predefined function of absolute value */
R friendlyMargin(R v) = ( v^2/(2*bo()) + tau()*v ).
R stopDist(R v) = (v^2 / (2*b()) + V()*v/b()).
R accelComp(R v) = ((A()/b() + 1) * (A()/2 * ep()^2 + ep()*(v+V))).
R admissibleSeparation(R v) = (stopDist(v) + friendlyMargin(V()) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
& tau() >= 0
& bo() > 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (abs(x-xo) > friendlyMargin(V()) | abs(y-yo) > friendlyMargin(V()))
& vxo^2+vyo^2<=V()^2
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v)+friendlyMargin(V()) | abs(y-yo) > stopDist(v)+friendlyMargin(V()))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R vo. /* refined obstacle: speed, acceleration, and direction */
R ao.
R dxo.
R dyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V()^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
t := 0;
}
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep() & v >= 0
}
}*@invariant(loopinv())
]( (v>0 -> (x - xo)^2 + (y - yo)^2 > (friendlyMargin(V()))^2) /* robot ensures friendly margin */
& ( 0<=vo & vo^2=vxo^2+vyo^2 & dxo*vo=vxo & dyo*vo=vyo /* obstacle can stop */
& (x - xo)^2 + (y - yo)^2 > (friendlyMargin(V()))^2
->
<{
ao := *; ?-bo() <= ao & vo + ao*ep() <= V();
t := 0;
{xo'=vo*dxo, yo'=vo*dyo, vo'=ao, t'=1 & vo>=0 & t<=ep()}
}*>((x-xo)^2 + (y-yo)^2 > 0 & vo=0))
)
End.
Tactic "Proof Theorem 3: Passive Friendly Safety".
tactic obstacleCanStop as (
unfold ; cut({`vo=0|dxo^2+dyo^2=1`}) ; <(
cut({`vo<=V()`}) ; <(
hideL('L=={`vo^2=vxo^2+vyo^2`}) ; hideL('L=={`vxo^2+vyo^2<=V()^2`});
con({`v`}, {`(vo=0|dxo^2+dyo^2=1)&bo()>0&ep()>0&(x-xo)^2+(y-yo)^2>(vo^2/(2*bo()))^2&0<=vo&vo<=V()&(v*ep()*bo()>=vo|vo=0)`}, 1); <(
QE,
QE,
unfold ; existsR({`-bo()`}, 1) ; unfold ; <(
QE
,
solve(1) ; existsR({`min((vo/bo(),ep()))`}, 1) ; abbrv({`min((vo/bo(),ep()))`}, {`minT`}) ; minmax(-14.1) ;
orL('L=={`vo=0|dxo^2+dyo^2=1`}) ; doall(QE)
)
)
,
hideR(1) ; QE
),
hideR(1) ; QE
)
);
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
diffInvariant({`-t*V() <= xo - old(xo) & xo - old(xo) <= t*V()`}, 1);
diffInvariant({`-t*V() <= yo - old(yo) & yo - old(yo) <= t*V()`}, 1)
);
tactic dib as (
diall;
diffInvariant({`v = old(v) - b()*t`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= x - old(x) & x - old(x) <= t * (v + b()/2*t)`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= y - old(y) & y - old(y) <= t * (v + b()/2*t)`}, 1)
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
diffInvariant({`v = old(v) + A()*t`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= x - old(x) & x - old(x) <= t * (v - A()/2*t)`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= y - old(y) & y - old(y) <= t * (v - A()/2*t)`}, 1)
);
tactic dw as (andL('L)*; dW(1));
tactic xAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+fm+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+fm+(A()/b()+1)*(A()/2*ep()^2+ep()*(v_0+V()))`});
hideR('R=={`abs(y-yo)>stopDist(v)+fm`});
smartQE; /* needs QE({`Mathematica`}) */
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
print({`Transforming...`});
transform({`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+fm+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+fm+(A()/b()+1)*(A()/2*ep()^2+ep()*(v_0+V()))`});
hideR('R=={`abs(x-xo)>stopDist(v)+fm`});
smartQE; /* needs QE({`Mathematica`}) */
print({`Proved acc arithmetic`})
);
tactic robotAlwaysStops as (
loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`});
abbrv({`(V()^2/(2*bo())+tau()*V())`}, {`fm`});
cut({`fm>=0`}); <(hideL('L=={`fm=(V()^2/(2*bo())+tau()*V())`}), hideR(1); QE);
dib; dw; prop; doall(smartQE); print({`Braking branch done`})
,
print({`Stopped branch`});
abbrv({`(V()^2/(2*bo())+tau()*V())`}, {`fm`});
cut({`fm>=0`}); <(hideL('L=={`fm=(V()^2/(2*bo())+tau()*V())`}), hideR(1); QE);
di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`v>0 -> abs(x-xo_0)>stopDist(v)+friendlyMargin(V()) | abs(y-yo_0)>stopDist(v)+friendlyMargin(V())`});
abbrv({`(V()^2/(2*bo())+tau()*V())`}, {`fm`});
cut({`fm>=0`}); <(hideL('L=={`fm=(V()^2/(2*bo())+tau()*V())`}), hideR(1); QE);
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Robot done`})
);
implyR(1) ; andL('L)* ; boxAnd(1) ; andR(1) ; <(
robotAlwaysStops ; done
,
MR({`vxo^2+vyo^2<=V()^2`},1); <(
loop({`vxo^2+vyo^2<=V()^2`}, 1); <(
id ; done,
id ; done,
composeb(1) ; GV(1.1) ; composeb(1) ; GV(1.1) ; master ; done
)
,
andL('L)* ;
hideL('L=={`A()>=0`});
hideL('L=={`b()>0`});
obstacleCanStop
)
)
End.
End.
Theorem "Theorem 4: Passive orientation safety".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R Gamma(). /* Sensor range in radian */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = ( v^2 / (2*b()) ).
R stopMargin(R v) = ( stopDist(v) + V()*v/b() ).
R accelComp(R v) = ( (A()/b() + 1) * (A()/2 * ep()^2 + ep()*v) ).
R accelMargin(R v) = ( accelComp(v) + (A()/b() + 1)*ep()*V() ).
R admissibleSeparation(R v) = ( stopMargin(v) + accelMargin(v) ).
R admissibleTurnLength(R v) = ( stopDist(v) + accelComp(v) ).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B isVisible(R) <-> ((.)>0). /* Indicates whether or not the obstacle is visible for the robot at the decision. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
& Gamma() > 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& beta = 0
& r != 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& r != 0
& (v>0 -> ( (abs(x-xo) > stopMargin(v) | abs(y-yo) > stopMargin(v))
| (!isVisible(visDeg) & abs(beta) + stopDist(v)/abs(r) < Gamma() )) )
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
R beta. /* Angle that the robot traveled since it last chose a new curve */
R visDeg. /* Indicates the "degree" to which the obstacle is visible to the robot (input to isVisible) */
End.
Problem.
assumptions() -> [
{
{
/* obstacle control */
{
vxo := *;
vyo := *;
?vxo^2+vyo^2 <= V()^2;
}
/* robot control */
{
/* brake on current curve. If the velocity is zero this just means that the robot remains stopped */
{a := -b();}
++ /* When we are stopped, both translational and rotational acceleration are 0 */
{?v=0; a := 0; w := 0;}
++ /* or choose a new safe curve */
{a := A();
beta := 0;
r :=*; ?r!=0;
/* measure obstacle position and whether or not it is visible to the robot */
xo := *; yo := *; visDeg := *;
?(isVisible(visDeg) ->
( abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v)) );
?admissibleTurnLength(v) < Gamma()*abs(r);
}
}
/* Reset the clocks */
t := 0;
/* Set w according to physics (rigid body motion) */
w :=*; ?w*r = v;
}
{x' = v * dx, y' = v * dy, dx' = -w * dy, dy' = w * dx, v' = a, w' = a/r, beta'=w,
xo' = vxo, yo' = vyo, t' = 1 & (t <= ep & v >= 0)}
}*
] (v > 0 -> ((x - xo)^2 + (y - yo)^2 > 0 | (!isVisible(visDeg) & (abs(beta) < Gamma()))) )
End.
Tactic "Proof Theorem 4: Passive orientation safety".
tactic dIHide as (
hideL('L~={`v>0->(abs(x-xo)>v^2/(2*b())+V()*v/b()|abs(y-yo)>v^2/(2*b())+V()*v/b())|!visDeg>0&abs(beta)+v^2/(2*b())/abs(r) < Gamma()`})*
);
tactic diall as (
print({`diall`});
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
dC({`(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V())
& (-t*V() <= yo - old(yo) & yo - old(yo) <= t*V())`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)));
diffInvariant({`w*r=v`}, 1)
);
tactic dib as (
diall;
diffInvariant({`v = old(v) - b()*t`}, 1);
diffInvariant({`beta = old(beta) + t/r*(v + b()/2*t)`}, 1);
dC({`(-t * (v + b()/2*t) <= x - old(x) & x - old(x) <= t * (v + b()/2*t))
& (-t * (v + b()/2*t) <= y - old(y) & y - old(y) <= t * (v + b()/2*t))`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`beta = old(beta)`}, 1);
dC({`x = old(x) & y = old(y)`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dia as (
diall;
diffInvariant({`v = old(v) + A()*t`}, 1);
diffInvariant({`beta = old(beta) + t/r*(v - A()/2*t)`}, 1);
dC({`(-t * (v - A()/2*t) <= x - old(x) & x - old(x) <= t * (v - A()/2*t))
& (-t * (v - A()/2*t) <= y - old(y) & y - old(y) <= t * (v - A()/2*t))`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
tactic qeHide as (
hideL('L~={`w*r=v`})*;
hideL('L~={`dx^2+dy^2=1`})*
);
tactic xAccArith as (
hideR('R=={`abs(y-yo)>stopMargin(v)`});
hideL('L=={`-t*(v-A()/2*t)<=y-y_0`});
hideL('L=={`y-y_0<=t*(v-A()/2*t)`});
hideL('L=={`-t*V()<=yo-yo_0`});
hideL('L=={`yo-yo_0<=t*V()`});
print({`Transforming...`});
transform({`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+((A()/b()+1)*(A()/2*t^2+t*v_0)+(A()/b()+1)*t*V())`}, 'L=={`abs(x_0-xo_0)>admissibleSeparation(v_0)`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
hideR('R=={`abs(x-xo)>stopMargin(v)`});
hideL('L=={`-t*(v-A()/2*t)<=x-x_0`});
hideL('L=={`x-x_0<=t*(v-A()/2*t)`});
hideL('L=={`-t*V()<=xo-xo_0`});
hideL('L=={`xo-xo_0<=t*V()`});
print({`Transforming...`});
transform({`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+((A()/b()+1)*(A()/2*t^2+t*v_0)+(A()/b()+1)*t*V())`}, 'L=={`abs(y_0-yo_0)>admissibleSeparation(v_0)`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop ; doall(qeHide; smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(qeHide; smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`v>0->((abs(x-xo_0)>stopMargin(v)|abs(y-yo_0)>stopMargin(v))|!isVisible(visDeg_0)&abs(beta_0)+stopDist(v)/abs(r_0) < Gamma())`});
unfold;
dia; dw;
print({`Acceleration arithmetic`});
implyR(1) ; andL('L)* ; fullSimplify ; implyR(1) ; orR(1) ; orR(1) ;
implyL('L=={`isVisible(visDeg) -> ( abs(x_0-xo_0) > admissibleSeparation(v_0) | abs(y_0-yo_0) > admissibleSeparation(v_0))`}) ; <(
hideR('R=={`abs(x-xo)>stopMargin(v)`}) ; hideR('R=={`abs(y-yo)>stopMargin(v)`}) ; andR(1) ; doall(smartQE)
,
print({`Acc Distance`});
hideL('L=={`admissibleTurnLength(v_0) < Gamma()*abs(r)`}) ;
hideR('R=={`visDeg<=0 & abs(beta) + stopDist(v)/abs(r) < Gamma()`});
hideL('L=={`r_0!=0`});
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`dx^2+dy^2=1`});
hideL('L=={`Gamma()>0`});
hideL('L=={`beta_0=0`});
hideL('L=={`w*r=v`});
hideL('L=={`beta=beta_0+t/r*(v-A()/2*t)`});
orL('L=={`abs(x_0-xo_0)>admissibleSeparation(v_0) | abs(y_0-yo_0)>admissibleSeparation(v_0)`}); <(
xAccArith
,
yAccArith
)
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 5: Passive safety with actual acceleration".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (v^2 / (2*b()) + V()*v/b()).
R accelComp(R v, R a) = ((a/b() + 1) * (a/2 * ep()^2 + ep()*(v+V))).
R admissibleSeparationG(R v, R a) = (stopDist(v) + accelComp(v,a)).
R admissibleSeparationL(R v, R a) = (-v^2/(2*a)-V*v/a).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := *; ?-b<=a & a<=A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
if (v+a*ep>=0) { ?abs(x-xo) > admissibleSeparationG(v,a) | abs(y-yo) > admissibleSeparationG(v,a); }
else { ?abs(x-xo) > admissibleSeparationL(v,a) | abs(y-yo) > admissibleSeparationL(v,a); }
}
};
t := 0;
}
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 5: Passive safety with actual acceleration".
tactic dIHide as (
hideL('L~={`v>0->abs(x-xo_0)>v^2/(2*b())+V()*v/b()|abs(y-yo_0)>v^2/(2*b())+V()*v/b()`})*;
hideL('L~={`abs(x-xo)>v^2/(2*b())+V()*v/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v+V()))|abs(y-yo)>v^2/(2*b())+V()*v/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v+V()))`})*
);
tactic diall as (
diffInvariant({`t>=0`}, 'R);
diffInvariant({`isWellformedDir()`}, 'R);
dC({`(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V())
& (-t*V() <= yo - old(yo) & yo - old(yo) <= t*V())`}, 'R); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dib as (
diall;
diffInvariant({`v = old(v) - b()*t`}, 'R);
diffInvariant({`-t * (v + b()/2*t) <= x - old(x) & x - old(x) <= t * (v + b()/2*t)`}, 'R);
diffInvariant({`-t * (v + b()/2*t) <= y - old(y) & y - old(y) <= t * (v + b()/2*t)`}, 'R)
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 'R);
diffInvariant({`x = old(x)`}, 'R);
diffInvariant({`y = old(y)`}, 'R)
);
tactic dia as (
diall;
diffInvariant({`v = old(v) + a*t`}, 'R);
diffInvariant({`-t * (v - a/2*t) <= x - old(x) & x - old(x) <= t * (v - a/2*t)`}, 'R);
diffInvariant({`-t * (v - a/2*t) <= y - old(y) & y - old(y) <= t * (v - a/2*t)`}, 'R)
);
tactic dw as (andL('L)*; dW('R));
tactic xAccArith as (
andL('L)*;
print({`Transforming...`});
?(transform({`abs(x_0-xo_0)>stopDist(v_0) + (a/b+1)*(a/2*t^2 + t*(v_0+V))`}, 'L=={`abs(x_0-xo_0)>stopDist(v_0) + (a/b+1)*(a/2*ep^2 + ep*(v_0+V))`}));
hideL('L~={`dx^2+dy^2=1`})*;
hideL('L~={`r*w=v`})*;
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
print({`Transforming...`});
?(transform({`abs(y_0-yo_0)>stopDist(v_0) + (a/b+1)*(a/2*t^2 + t*(v_0+V))`}, 'L=={`abs(y_0-yo_0)>stopDist(v_0) + (a/b+1)*(a/2*ep^2 + ep*(v_0+V))`}));
hideL('L~={`dx^2+dy^2=1`})*;
hideL('L~={`r*w=v`})*;
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Free driving non-stopping branch`});
hideL('L == {`v>0 -> abs(x-xo_0)>stopDist(v) | abs(y-yo_0)>stopDist(v)`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Free driving non-stopping branch done`})
,
print({`Free driving stopping branch`});
hideL('L == {`v>0 -> abs(x-xo_0)>stopDist(v) | abs(y-yo_0)>stopDist(v)`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Free driving stopping branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 6: Passive safety despite location uncertainty".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R Dp(). /* maximum location uncertainty */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (v^2 / (2*b()) + V()*v/b()).
R accelComp(R v) = ((A()/b() + 1) * (A()/2 * ep()^2 + ep()*(v+V())) + Dp()).
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
& Dp() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R mx. /* robot measured position: x */
R my. /* robot measured position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* locate */
{
mx := *; my := *;
?(mx-x)^2+(my-y)^2 <= Dp()^2;
}
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(mx-xo) > admissibleSeparation(v)
| abs(my-yo) > admissibleSeparation(v);
}
};
t := 0;
}
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 6: Passive safety despite location uncertainty".
tactic dIHide as (
hideL('L~={`v>0->abs(x-xo_0)>v^2/(2*b())+V()*v/b()|abs(y-yo_0)>v^2/(2*b())+V()*v/b()`})*;
hideL('L~={`abs(mx-xo)>v^2/(2*b())+V()*v/b()+((A()/b()+1)*(A()/2*ep()^2+ep()*(v+V()))+Dp())|abs(my-yo)>v^2/(2*b())+V()*v/b()+((A()/b()+1)*(A()/2*ep()^2+ep()*(v+V()))+Dp())`})*
);
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
dC({`(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V())
& (-t*V() <= yo - old(yo) & yo - old(yo) <= t*V())`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dib as (
diall;
diffInvariant({`v = old(v) - b()*t`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= x - old(x) & x - old(x) <= t * (v + b()/2*t)`}, 1);
diffInvariant({`-t * (v + b()/2*t) <= y - old(y) & y - old(y) <= t * (v + b()/2*t)`}, 1)
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
diffInvariant({`v = old(v) + A()*t`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= x - old(x) & x - old(x) <= t * (v - A()/2*t)`}, 1);
diffInvariant({`-t * (v - A()/2*t) <= y - old(y) & y - old(y) <= t * (v - A()/2*t)`}, 1)
);
tactic dw as (andL('L)*; dW(1));
tactic xAccArith as (
andL('L)*;
hideL('L~={`r*w=v`})*;
hideL('L~={`dx^2+dy^2=1`})*;
hideL('L=={`vxo^2+vyo^2<=V()^2`});
print({`Transforming...`});
transform({`abs(mx-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))+Dp()`}, 'L=={`abs(mx-xo_0)>admissibleSeparation(v_0)`});
hideL('L=={`t<=ep()`});
transform({`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(mx-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))+Dp()`});
hideL('L=={`(mx-x_0)^2+(my-y_0)^2<=Dp()^2`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
hideL('L~={`r*w=v`})*;
hideL('L~={`dx^2+dy^2=1`})*;
hideL('L=={`vxo^2+vyo^2<=V()^2`});
print({`Transforming...`});
transform({`abs(my-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))+Dp()`}, 'L=={`abs(my-yo_0)>admissibleSeparation(v_0)`});
hideL('L=={`t<=ep()`});
transform({`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(my-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))+Dp()`});
hideL('L=={`(mx-x_0)^2+(my-y_0)^2<=Dp()^2`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L == {`v>0 -> abs(x-xo_0)>stopDist(v) | abs(y-yo_0)>stopDist(v)`});
dia; dw;
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 7: Passive safety despite actuator perturbation".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R Da(). /* maximum actuator perturbation 0< Da <= 1 (robot will not loose brakes entirely) */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = ( v^2 / (2*(b()*Da())) + V()*v/(b()*Da()) ).
R accelComp(R v) = ( (A()/(b()*Da()) + 1) * (A()/2 * ep()^2 + ep()*(v+V())) ).
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
& 0 < Da() & Da() <= 1
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot control choice: translational acceleration */
R da. /* robot actuator disturbance */
R acc. /* robot actual translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
/* actuator perturbation */
{
da := *; ?(Da<=da & da<=1); acc := da*a;
};
t := 0;
}
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = acc, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = acc/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 7: Passive safety despite actuator perturbation".
tactic dIHide as (
hideL('L~={`v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v)`})*;
hideL('L~={`abs(x-xo)>admissibleSeparation(v)|abs(y-yo)>admissibleSeparation(v)`})*
);
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
dC({`(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V())
& (-t*V() <= yo - old(yo) & yo - old(yo) <= t*V())`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dib as (
diall;
dC({`v <= old(v) - (b()*Da())*t`}, 1); <(nil, dIHide; dI(1));
dC({`(-t * (old(v) - (b()*Da())/2*t) <= x - old(x) & x - old(x) <= t * (old(v) - (b()*Da())/2*t))
& -t * (old(v) - (b()*Da())/2*t) <= y - old(y) & y - old(y) <= t * (old(v) - (b()*Da())/2*t)`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
dC({`v <= old(v) + A()*t`}, 1); <(nil, dIHide; dI(1));
dC({`(-t * (old(v) + A()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) + A()/2*t))
& (-t * (old(v) + A()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) + A()/2*t))`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
tactic xAccArith as (
andL('L)*;
hideL('L=={`r!=0`});
hideL('L=={`r*w_0=v_0`});
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`dx^2+dy^2=1`});
hideL('L=={`dx_0^2+dy_0^2=1`});
hideL('L=={`-t*(v_0+A()/2*t)<=y-y_0`});
hideL('L=={`y-y_0<=t*(v_0+A()/2*t)`});
hideL('L=={`-t*V()<=yo-yo_1`});
hideL('L=={`yo-yo_1<=t*V()`});
print({`Transforming...`});
transform({`abs(x_0-xo_1)>v_0^2/(2*(b()*Da()))+V()*v_0/(b()*Da())+(A()/(b()*Da())+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L~={`abs(x-xo)>admissibleSeparation(v)`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
abbrv({`b*Da()`},{`actB`}); cut({`actB>0`}); <(hideL('L=={`actB=b*Da()`}), hideR(1); smartQE);
hideL('L=={`t<=ep()`});
hideL('L=={`b()>0`});
hideL('L=={`ep()>0`});
hideL('L=={`0<Da()`});
hideL('L=={`Da()<=1`});
hideL('L=={`Da()<=da`});
hideL('L=={`da<=1`});
hideL('L=={`v>=0`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
andL('L)*;
hideL('L=={`r!=0`});
hideL('L=={`r*w_0=v_0`});
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`dx^2+dy^2=1`});
hideL('L=={`dx_0^2+dy_0^2=1`});
hideL('L=={`-t*(v_0+A()/2*t)<=x-x_0`});
hideL('L=={`x-x_0<=t*(v_0+A()/2*t)`});
hideL('L=={`-t*V()<=xo-xo_1`});
hideL('L=={`xo-xo_1<=t*V()`});
print({`Transforming...`});
transform({`abs(y_0-yo_1)>v_0^2/(2*(b()*Da()))+V()*v_0/(b()*Da())+(A()/(b()*Da())+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L~={`abs(y-yo)>admissibleSeparation(v)`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
abbrv({`b*Da()`},{`actB`}); cut({`actB>0`}); <(hideL('L=={`actB=b*Da()`}), hideR(1); smartQE);
hideL('L=={`t<=ep()`});
hideL('L=={`b()>0`});
hideL('L=={`ep()>0`});
hideL('L=={`0<Da()`});
hideL('L=={`Da()<=1`});
hideL('L=={`Da()<=da`});
hideL('L=={`da<=1`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; abbrv({`b*Da()`},{`actB`}); cut({`actB>0`}); <(hideL('L=={`actB=b*Da()`}), hideR(1); smartQE);
prop;
doall(hideL('L=={`dx^2+dy^2=1`}); hideL('L=={`dx_0^2+dy_0^2=1`}); hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`t<=ep()`}); hideL('L=={`ep()>0`}); hideL('L=={`A()>=0`});
print({`Braking QE`}); smartQE);
print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(print({`Stopped QE`}); smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
dia; dw;
hideL('L~={`v>0->abs(x-xo)>v^2/(2*(b()*Da()))+V()*v/(b()*Da())|abs(y-yo)>v^2/(2*(b()*Da()))+V()*v/(b()*Da())`});
prop; <(
xAccArith,
yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 8: Passive safety despite velocity uncertainty".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R Dv(). /* maximum velocity uncertainty */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = ( v^2 / (2*b()) + V()*v/b() ).
R accelComp(R v) = ( (A()/b() + 1) * (A()/2 * ep()^2 + ep()*(v+V())) ).
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
& Dv() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R mv. /* robot measured velocity */
R a. /* robot control choice: translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* sense */
{
mv := *; ?0<=mv & v-Dv()<=mv & mv<=v+Dv();
}
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(mv+Dv())
| abs(y-yo) > admissibleSeparation(mv+Dv());
}
};
t := 0;
}
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 8: Passive safety despite velocity uncertainty".
tactic dIHide as (
hideL('L~={`v>0->abs(x-xo)>v^2/(2*b())+V()*v/b()|abs(y-yo)>v^2/(2*b())+V()*v/b()`})*;
hideL('L~={`abs(x-xo)>(mv+Dv())^2/(2*b())+V()*(mv+Dv())/b()+(A()/b()+1)*(A()/2*ep()^2+ep()*(mv+Dv()+V()))|abs(y-yo)>(mv+Dv())^2/(2*b())+V()*(mv+Dv())/b()+(A()/b()+1)*(A()/2*ep()^2+ep()*(mv+Dv()+V()))`})*
);
tactic preQEHide as (
andL('L)*;
hideL('L~={`dx^2+dy^2=1`})*2;
hideL('L~={`vxo^2+vyo^2<=V()^2`})
);
tactic diall as (
diffInvariant({`t>=0`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
dC({`(-t*V() <= xo - old(xo) & xo - old(xo) <= t*V())
& (-t*V() <= yo - old(yo) & yo - old(yo) <= t*V())`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dib as (
diall;
dC({`v <= old(v) - b()*t`}, 1); <(nil, dIHide; dI(1));
dC({`(-t * (old(v) - b()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) - b()/2*t))
& (-t * (old(v) - b()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) - b()/2*t))`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
dC({`v <= old(v) + A()*t`}, 1); <(nil, dIHide; dI(1));
dC({`(-t * (old(v) + A()/2*t) <= x - old(x) & x - old(x) <= t * (old(v) + A()/2*t))
& (-t * (old(v) + A()/2*t) <= y - old(y) & y - old(y) <= t * (old(v) + A()/2*t))`}, 1); <(nil, dIHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
tactic xAccArith as (
hideL('L=={`-t*(v_0+A()/2*t)<=y-y_0`});
hideL('L=={`y-y_0<=t*(v_0+A()/2*t)`});
hideL('L=={`-t*V()<=yo-yo_0`});
hideL('L=={`yo-yo_0<=t*V()`});
hideL('L=={`r!=0`});
hideL('L=={`r*w_0=v_0`});
hideL('L=={`-W()<=w_0`});
hideL('L=={`w_0<=W()`});
print({`Transforming...`});
transform({`abs(x_0-xo_0)>(mv+Dv())^2/(2*b())+V()*(mv+Dv())/b()+(A()/b()+1)*(A()/2*t^2+t*((mv+Dv())+V()))`}, 'L~={`abs(x-xo)>admissibleSeparation(mv+Dv())`});
hideL('L=={`t<=ep()`});
hideL('L=={`ep()>0`});
hideR('R=={`abs(y-yo)>stopDist(v)`});
transform({`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L~={`abs(x_0-xo_0)>(mv+Dv())^2/(2*b())+V()*(mv+Dv())/b()+(A()/b()+1)*(A()/2*t^2+t*((mv+Dv())+V()))`});
smartQE;
print({`Proved acc arithmetic`})
);
tactic yAccArith as (
hideL('L=={`-t*(v_0+A()/2*t)<=x-x_0`});
hideL('L=={`x-x_0<=t*(v_0+A()/2*t)`});
hideL('L=={`-t*V()<=xo-xo_0`});
hideL('L=={`xo-xo_0<=t*V()`});
hideL('L=={`r!=0`});
hideL('L=={`r*w_0=v_0`});
hideL('L=={`-W()<=w_0`});
hideL('L=={`w_0<=W()`});
print({`Transforming...`});
transform({`abs(y_0-yo_0)>(mv+Dv())^2/(2*b())+V()*(mv+Dv())/b()+(A()/b()+1)*(A()/2*t^2+t*((mv+Dv())+V()))`}, 'L~={`abs(y-yo)>admissibleSeparation(mv+Dv())`});
hideL('L=={`t<=ep()`});
hideL('L=={`ep()>0`});
hideR('R=={`abs(x-xo)>stopDist(v)`});
transform({`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L~={`abs(y_0-yo_0)>(mv+Dv())^2/(2*b())+V()*(mv+Dv())/b()+(A()/b()+1)*(A()/2*t^2+t*((mv+Dv())+V()))`});
smartQE;
print({`Proved acc arithmetic`})
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); dib; dw; prop; doall(print({`Braking QE`}); preQEHide; smartQE); print({`Braking branch done`})
,
print({`Stopped branch`}); di0; dw; prop; doall(preQEHide; smartQE); print({`Stopped branch done`})
,
print({`Acceleration branch`});
hideL('L~={`v>0 -> abs(x-xo)>stopDist(v) | abs(y-yo)>stopDist(v)`});
dia; dw;
prop; <(
preQEHide; xAccArith,
preQEHide; yAccArith
);
print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 9: Passive safety for asynchronous controllers".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (v^2 / (2*b()) + V()*v/b()).
R accelComp(R v) = ((A()/b() + 1) * (A()/2 * ep()^2 + ep()*(v+V))).
R admissibleSeparation(R v) = (stopDist(v) + accelComp(v)).
B isWellformedDir() <-> (dx^2 + dy^2 = 1). /* The orientation of the robot is a unit vector. */
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v))
).
/* todo invariant lookup for inner fails */
B innerloopinv() <-> (
0<=t & t<=ep()
& v >= 0
& isWellformedDir()
& -t*V() <= xo - old(xo) & xo - old(xo) <= t*V() /* todo: old(.) support in loop invariants */
& -t*V() <= yo - old(yo) & yo - old(yo) <= t*V()
& -t * (v - a/2*t) <= x - old(x) & x - old(x) <= t * (v - a/2*t)
& -t * (v - a/2*t) <= y - old(y) & y - old(y) <= t * (v - a/2*t)
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; }
++
/* or choose a new safe curve */
{ a := A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?r!=0 & r*w = v;
/* use that curve, if it is a safe one (admissible velocities) */
? abs(x-xo) > admissibleSeparation(v)
| abs(y-yo) > admissibleSeparation(v);
}
};
t := 0;
}
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
};
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}
}*@invariant(innerloopinv())
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 9: Passive safety for asynchronous controllers".
tactic dibHide as (
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`dx^2+dy^2=1`});
hideL('L~={`-t*V()<=xo-old(xo)`})*2;
hideL('L~={`xo-old(xo)<=t*V()`})*2;
hideL('L~={`-t*(v+b()/2*t)<=x-old(x)`})*2;
hideL('L~={`x-old(x)<=t*(v+b()/2*t)`})*2
);
tactic diaHide as (
hideL('L=={`vxo^2+vyo^2<=V()^2`});
hideL('L=={`dx^2+dy^2=1`});
hideL('L~={`-t*V()<=xo-old(xo)`})*2;
hideL('L~={`xo-old(xo)<=t*V()`})*2;
hideL('L~={`-t*(v-A()/2*t)<=x-old(x)`})*2;
hideL('L~={`x-old(x)<=t*(v-A()/2*t)`})*2
);
tactic diall as (
diffInvariant({`t>=old(t)`}, 1);
diffInvariant({`isWellformedDir()`}, 1);
diffInvariant({`-(t-old(t))*V() <= xo - old(xo) & xo - old(xo) <= (t-old(t))*V()`}, 1);
diffInvariant({`-(t-old(t))*V() <= yo - old(yo) & yo - old(yo) <= (t-old(t))*V()`}, 1)
);
tactic dib as (
diall;
dC({`v = old(v) - b()*(t-old(t))`}, 1); <(nil, dibHide; dI(1));
dC({`(-(t-old(t)) * (v + b()/2*(t-old(t))) <= x - old(x) & x - old(x) <= (t-old(t)) * (v + b()/2*(t-old(t))))
& (-(t-old(t)) * (v + b()/2*(t-old(t))) <= y - old(y) & y - old(y) <= (t-old(t)) * (v + b()/2*(t-old(t))))`}, 1); <(nil, dibHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic di0 as (
diall;
diffInvariant({`v = old(v)`}, 1);
diffInvariant({`x = old(x)`}, 1);
diffInvariant({`y = old(y)`}, 1)
);
tactic dia as (
diall;
dC({`v = old(v) + A()*(t-old(t))`}, 1); <(nil, diaHide; dI(1));
dC({`(-(t-old(t)) * (v - A()/2*(t-old(t))) <= x - old(x) & x - old(x) <= (t-old(t)) * (v - A()/2*(t-old(t))))
& (-(t-old(t)) * (v - A()/2*(t-old(t))) <= y - old(y) & y - old(y) <= (t-old(t)) * (v - A()/2*(t-old(t))))`}, 1); <(nil, diaHide; boxAnd(1); andR(1); doall(dI(1)))
);
tactic dw as (andL('L)*; dW(1));
tactic ghosts as (
discreteGhost({`v`}, 1) ; discreteGhost({`x`}, 1) ; discreteGhost({`y`}, 1) ; discreteGhost({`xo`}, 1) ;
discreteGhost({`yo`}, 1) ; (assignEquality(1) ; allR2L('Llast))*5
);
tactic innerUseCase as (
andR(1) ; <(
prop,
andR(1) ; <(
prop,
implyR(1) ; orR(1) ; implyL('L=={`v_0>0 -> abs(x_0-xo_0) > stopDist(v_0) | abs(y_0-yo_0) > stopDist(v_0)`}) ; <(
QE,
orL('L=={`abs(x_0-xo_0) > stopDist(v_0) | abs(y_0-yo_0) > stopDist(v_0)`}) ; <(
hideR('R=={`abs(y-yo) > stopDist(v)`}); smartQE,
hideR('R=={`abs(x-xo) > stopDist(v)`}); smartQE
)
)
)
)
);
tactic brakingInnerLoop as (
ghosts;
loop({`0<=t&t<=ep()&v>=0&dx^2+dy^2=1&v=v_0-b()*t&-t*V()<=xo-xo_0&xo-xo_0<=t*V()&-t*V()<=yo-yo_0&yo-yo_0<=t*V()&-t*(v+b()/2*t)<=x-x_0&x-x_0<=t*(v+b()/2*t)&-t*(v+b()/2*t)<=y-y_0&y-y_0<=t*(v+b()/2*t)`}, 1) ; <(
QE,
innerUseCase,
unfold;
hideL('L=={`v_0>0 -> abs(x_0-xo_0) > stopDist(v_0) | abs(y_0-yo_0) > stopDist(v_0)`});
dib; dw; unfold; doall(smartQE)
)
);
tactic stoppedInnerLoop as (
ghosts;
loop({`0<=t&t<=ep()&v>=0&dx^2+dy^2=1&v=v_0&-t*V()<=xo-xo_0&xo-xo_0<=t*V()&-t*V()<=yo-yo_0&yo-yo_0<=t*V()&x=x_0&y=y_0`}, 1) ; <(
QE,
innerUseCase,
unfold;
hideL('L=={`v_0>0 -> abs(x_0-xo_0) > stopDist(v_0) | abs(y_0-yo_0) > stopDist(v_0)`});
di0; dw; unfold; doall(smartQE)
)
);
tactic accInnerLoop as (
hideL('L=={`v>0 -> abs(x-xo_0) > stopDist(v) | abs(y-yo_0) > stopDist(v)`}) ;
ghosts;
loop({`0<=t&t<=ep()&v>=0&dx^2+dy^2=1&v=v_0+A()*t&-t*V()<=xo-xo_0&xo-xo_0<=t*V()&-t*V()<=yo-yo_0&yo-yo_0<=t*V()&-t*(v-A()/2*t)<=x-x_0&x-x_0<=t*(v-A()/2*t)&-t*(v-A()/2*t)<=y-y_0&y-y_0<=t*(v-A()/2*t)`}, 1) ; <(
QE,
andR(1) ; <(
prop,
andR(1) ; <(
prop,
implyR(1) ; orR(1) ;
orL('L=={`abs(x_0-xo_0) > admissibleSeparation(v_0) | abs(y_0-yo_0) > admissibleSeparation(v_0)`}); <(
transform({`abs(x_0-xo_0) > v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(x_0-xo_0)>admissibleSeparation(v_0)`});
hideR('R=={`abs(y-yo) > stopDist(v)`}); smartQE
,
transform({`abs(y_0-yo_0) > v_0^2/(2*b())+V()*v_0/b()+(A()/b()+1)*(A()/2*t^2+t*(v_0+V()))`}, 'L=={`abs(y_0-yo_0)>admissibleSeparation(v_0)`});
hideR('R=={`abs(x-xo) > stopDist(v)`}); smartQE
)
)
),
unfold; hideL('L=={`abs(x_0-xo_0) > admissibleSeparation(v_0) | abs(y_0-yo_0) > admissibleSeparation(v_0)`});
dia; dw; unfold; doall(smartQE)
)
);
implyR(1); andL('L)*; loop({`loopinv()`}, 1); <(
print({`Base case...`}); smartQE; print({`Base case done`})
,
print({`Use case...`}); smartQE; print({`Use case done`})
,
print({`Induction step`}); unfold; <(
print({`Braking branch`}); brakingInnerLoop; print({`Braking branch done`})
,
print({`Stopped branch`}); stoppedInnerLoop; print({`Stopped branch done`})
,
print({`Acceleration branch`}); accInnerLoop; print({`Acceleration branch done`})
);
print({`Induction step done`})
);
done;
print({`Proof done`})
End.
End.
Theorem "Theorem 11: Reach waypoint".
/*
* Robot must stop within distance delta at goal.
*
* Robot
* - must stop within distance delta of goal
* - can only drive straight and forward
* - ensures progress towards goal
*
* Liveness property:
* - Robot can stop at goal
*
*/
Definitions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R GDelta(). /* goal area size */
R Vmax(). /* robot cannot go faster than this */
R waypointStartDist(R xg) = ( xg-GDelta() ).
R waypointEndDist(R xg) = ( xg+GDelta() ).
R minV() = ( A()*ep() ).
R stopDist(R v) = ( v^2/(2*b()) ).
R accComp(R v) = ( (A()/b() + 1)*(A()/2*ep()^2 + ep()*v) ).
B bounds() <-> ( /* Bounds for global constants */
A() > 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& Vmax() >= 2*A()*ep()
& GDelta() > Vmax()*ep() + Vmax()^2/(2*b()) /* waypoint is large enough that robot can
start driving and still stop inside */
).
B initialState() <-> ( /* Stopped somewhere safe initially */
vr = 0
& xr < waypointStartDist(xg)
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> (
0 <= vr & vr <= Vmax & xr + stopDist(vr) < waypointEndDist(xg)
).
HP ctrl ::= {
ar := -b();
++ ?vr = 0; ar := 0;
++ ?xr + stopDist(vr) + accComp(vr) < waypointEndDist(xg) & vr+A()*ep()<=Vmax(); ar := A();
++ ?xr <= waypointStartDist(xg) & vr <= Vmax(); ar := *; ?-b() <= ar & ar <= (Vmax()-vr)/ep() & ar <= A();
}.
HP dyn ::= { {xr' = vr, vr' = ar, t' = 1 & t <= ep() & vr >= 0} }.
HP dwwp ::= { { { ctrl; t:=0; } dyn; }*@invariant(loopinv()) }.
End.
ProgramVariables.
R xr. /* robot position: x */
R vr. /* robot translational velocity */
R ar. /* robot translational acceleration */
R xg. /* goal position */
R t. /* control cycle time */
End.
Problem.
assumptions()
->
/* safety */
[ dwwp; ] (xr < waypointEndDist(xg))
&
/* liveness */
< dwwp; >(waypointStartDist(xg) < xr)
End.
Tactic "Proof Theorem 11: Reach waypoint".
implyR(1) ; andL('L)* ; andR(1) ; <(
master,
iterated(1) ; orR(1) ; composed(2) ; composed(2) ; choiced(2) ; orR(2) ; hideR(2) ; choiced(2) ; orR(2) ;
hideR(2) ; choiced(2) ; orR(2) ; hideR(2) ; composed(2) ; testd(2) ; andR(2); <(
QE,
composed(2) ; randomd(2) ; existsR({`min(((Vmax()-vr)/ep(),A()))`}, 2) ; testd(2) ; andR(2) ; <(
QE,
assignd(2) ; solve(2) ; existsR({`ep()`}, 2) ; andR(2) ; <(
QE,
andR(2) ; <(
QE,
existsR({`ar*ep()+vr_1`}, 2) ; simplify(2) ;
existsR({`ar*(ep()^2/2)+vr_1*ep()+xr_1`}, 2) ; simplify(2) ;
con({`v`}, {`Vmax()>0&A()>0&b()>0&ep()>0&0 < vr&vr<=Vmax()&xg-GDelta() < xr+v*ep()*vr`}, 2) ; <(
QE,
QE,
composed(1) ; composed(1) ; cut({`xr<=xg-GDelta()|xg-GDelta() < xr`}) ; <(
orL('L=={`xr<=xg-GDelta()|xg-GDelta() < xr`}) ; <(
choiced(1) ; orR(1) ; hideR(1) ; choiced(1) ; orR(1) ; hideR(1) ; choiced(1) ; orR(1) ;
hideR(1) ; composed(1) ; testd(1) ; andR(1) ; <(
master,
composed(1) ; randomd(1) ; existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; solve(1) ; QE({`Mathematica`})
)
),
choiced(1) ; orR(1) ; hideR(2) ; assignd(1) ; assignd(1) ; solve(1) ;
andL('L)*;
/* hide duplicate facts */
hideL('L=={`b()>0`}); hideL('L=={`ep()>0`});
/* hide irrelevant facts */
hideL('L=={`vr_1=0`}); hideL('L=={`xr_1 < xg-GDelta()`}); hideL('L=={`A()>0`})*2;
hideL('L=={`Vmax()>=2*A()*ep()`}); hideL('L=={`GDelta()>Vmax()*ep()+Vmax()^2/(2*b())`});
QE({`Mathematica`})
),
hideR(1) ; QE
)
)
)
)
)
)
)
End.
End.
Theorem "Theorem 12: Cross intersection".
/*
* Robot must safely cross an intersection.
*
* Robot
* - must cross intersection safely
* - can only drive straight and forward
* - ensures progress towards intersection
*
* Obstacle
* - Drives forward with minimum speed (does not block intersection)
*
* Intersection
* - At position 0 (on both the robot's and the obstacle's path)
*
* Liveness property:
* - Robot can cross intersection
*
* Safety property:
* - Robot and obstacle are not at the intersection at the same time
*
*/
Definitions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R Vmin(). /* obstacle minimum speed */
R ixr() = ( 0 ). /* position of intersection on path of robot */
R ixo() = ( 0 ). /* position of intersection on path of obstacle */
R minV() = ( A()*ep() ).
R stopDist(R v) = ( v^2/(2*b()) ).
R accComp(R v) = ( (A()/b() + 1)*(A()/2*ep()^2 + ep()*v) ).
B OAfterX(R xo) <-> ( xo>ixo() ).
B RAfterX(R x) <-> ( x>ixr() ).
B bounds() <-> ( /* Bounds for global constants */
A() > 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& Vmin() > 0
).
B initialState() <-> ( /* Somewhere before intersection initially */
vr = 0
& vo>=Vmin()
& xr < ixr()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> (
0 <= vr & Vmin()<=vo & (RAfterX(xr) | OAfterX(xo) | xr + stopDist(vr) < ixr() |
(vr>0 & ( xo+vo*(ixr()-xr)/vr+A/2*((ixr()-xr)/vr)^2 < ixo()
| ixo() < xo + Vmin()*(ixr()-xr)/vr))
)
).
HP obstacle ::= { ao := *; ?-b()<=ao&ao<=A(); }.
HP robot ::= {
if (RAfterX(xr) | OAfterX(xo)) {
ar := *; ?-b()<=ar&ar<=A();
} else { if (/*PassFaster*/ vr>0 & ( xo+vo*(ixr()-xr)/vr+A()/2*((ixr()-xr)/vr)^2 < ixo()
| ixo() < xo + Vmin()*(ixr()-xr)/(vr+A()*ep()) ) ) {
ar := *; ?0<=ar&ar<=A();
} else { if (/*PassCoast*/ vr>0 & ixo() < xo + Vmin()*(ixr()-xr)/vr) {
ar := 0;
} else { /* 1D Model 3 */
ar := -b();
++ ?vr = 0; ar := 0;
++ ?xr + stopDist(vr) + accComp(vr) < ixr(); ar := A();
}}}
}.
HP dyn ::= { {xr' = vr, vr' = ar, xo'=vo, vo'=ao, t' = 1 & t <= ep() & vr >= 0 & vo>=Vmin() } }.
HP dwcx ::= {
{ obstacle;
{ robot; t := 0; }
dyn;
}*@invariant(loopinv())
}.
End.
ProgramVariables.
R xr. /* robot position: x */
R vr. /* robot translational velocity */
R ar. /* robot translational acceleration */
R xo. /* obstacle position */
R vo. /* obstacle velocity */
R ao. /* obstacle acceleration */
R t. /* control cycle time */
End.
Problem.
assumptions()
->
/* safety */
[ dwcx; ](xr=ixr() -> xo!=ixo())
&
/* liveness */
< dwcx; >(RAfterX(xr))
End.
Tactic "Proof Theorem 12: Cross intersection (single convergence condition)".
/* some of the QE need QE({`Mathematica`}) */
implyR(1) ; andR(1) ; <(
loop({`0<=vr&Vmin()<=vo&(xr>0|xo>0|xr+vr^2/(2*b()) < 0|vr>0&(xo+vo*(0-xr)/vr+A()/2*((0-xr)/vr)^2 < 0|0 < xo+Vmin()*(0-xr)/vr))`}, 1) ; <(
QE,
QE,
composeb(1) ; composeb(1.1) ; solve(1.1.1) ; chase(1) ; allR(1) ; implyR(1) ; andL(-1) ; andL(-7) ; andR(1) ; <(
implyR(1) ; allR(1) ; implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; orL(-9) ; <(
fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; hideR(2) ; QE
)
),
fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; hideR(3) ; hideR(1) ; QE
)
)
),
implyR(1) ; andR(1) ; <(
implyR(1) ; andL(-10) ; fullSimplify ; allR(1) ; implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; hideL(-7) ; hideR(3) ; andR(3) ; <(
QE,
orR(3) ; orL(-9) ; <(
hideR(4) ; hideL(-7) ; hideR(2) ; QE,
hideL(-7) ; hideR(3) ; hideR(2) ; QE
)
)
)
),
implyR(1) ; andR(1) ; <(
implyR(1) ; andL(-11) ; fullSimplify ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; orR(4) ; hideR(4) ; hideR(3) ; hideL(-7) ; hideL(-7) ; hideL(-7) ; QE
),
implyR(1) ; andR(1) ; <(
notOr(-9) ; andL(-9) ; notAnd(-9) ; notAnd(-10) ; fullSimplify ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; orL(-8) ; <(
hideR(4) ; hideR(1) ; hideR(1) ; hideL(-9) ; hideL(-9) ; QE,
andL(-8) ; fullSimplify ; fullSimplify ; closeFalse
)
)
),
andR(1) ; <(
implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; fullSimplify ; andR(1) ; <(
QE,
QE
),
implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; hideL(-10) ; hideL(-10) ; hideL(-9) ; hideL(-8) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; hideR(4) ; hideR(1) ; hideR(1) ; QE
)
)
)
)
)
)
)
),
con({`v`}, {`A()>0&b()>0&ep()>0&Vmin()>0&vo>=Vmin()&vr>=0&(xo<=0->vr=0)&\exists n (n>=2&xo+(v-n)*ep()*Vmin()>0&vr+(min((v,n-1))-(n-2))*ep()*A()>=A()*ep()&(xr>0|xr+min((v,n-2))*ep()*(A()*ep())>0))`}, 1) ; <(
QE,
QE,
composed(1) ; composed(1.1) ; solve(1.1.1) ; composed(1) ; randomd(1) ; existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
composed(1) ; ((andL('L) | existsL('L))*) ; choiced(1) ; orR(1) ; composed(1) ; testd(1) ; orL(-16=={`xr>0|xr+min((v,n-2))*ep()*(A()*ep())>0`}) ; <(
hideR(2) ; fullSimplify ; composed(1) ; randomd(1) ; implyL(-8=={`xo<=0->vr=0`}) ; <(
cut({`xo+vo*ep()>0|xo+vo*ep()<=0`}) ; <(
orL('Llast) ; <(
existsR({`A()`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; andR(1) ; <(
QE,
existsR({`n`}, 1) ; fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
QE
)
)
)
)
)
),
hideR(1) ; QE
),
hideR(1) ; QE
),
cut({`xo+vo*ep()>0|xo+vo*ep()<=0`}) ; <(
orL('Llast) ; <(
existsR({`A()`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; andR(1) ; <(
QE,
existsR({`n`}, 1) ; fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
QE
)
)
)
)
)
),
existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; existsR({`n`}, 1) ; fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
QE
)
)
)
)
)
),
hideR(1) ; QE
)
),
composed(2) ; testd(2) ; implyL(-12=={`xo<=0->vr=0`}) ; <(
andR(1) ; <(
hideR(2) ; QE,
hideR(2) ; composed(1) ; randomd(1) ; existsR({`A()`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; andR(1) ; <(
QE,
existsR({`n`}, 1) ; fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
QE
)
)
)
)
)
)
),
andR(1) ; <(
andR(2) ; <(
QE,
choiced(2) ; orR(2) ; hideR(2) ; composed(2) ; testd(2) ; andR(2) ; <(
QE,
choiced(2) ; orR(2) ; hideR(2) ; composed(2) ; testd(2) ; andR(2) ; <(
QE,
choiced(2) ; orR(2) ; hideR(2) ; choiced(2) ; orR(2) ; hideR(3) ; composed(2) ; testd(2) ; fullSimplify ; assignd(2) ; assignd(2) ; existsR({`ep()`}, 2) ; andR(2) ; <(
QE,
andR(2) ; <(
QE,
fullSimplify ; existsR({`n`}, 2) ; fullSimplify ; andR(2) ; <(
QE,
andR(2) ; <(
QE,
QE
)
)
)
)
)
)
),
hideR(2) ; composed(1) ; randomd(1) ; cut({`xo+vo*ep()>0|xo+vo*ep()<=0`}) ; <(
orL('Llast) ; <(
existsR({`A()`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; andR(1) ; <(
QE,
existsR({`n`}, 1) ; fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
QE
)
)
)
)
)
),
existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; existsR({`n`}, 1) ; fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
QE
)
)
)
)
)
),
hideR(1) ; QE
)
)
)
)
)
)
)
End.
Tactic "Proof Theorem 12: Cross intersection (loop split and unroll)".
/* some of the QE need QE({`Mathematica`}) */
implyR(1) ; andR(1) ; <(
loop({`0<=vr&Vmin()<=vo&(xr>0|xo>0|xr+vr^2/(2*b()) < 0|vr>0&(xo+vo*(0-xr)/vr+A()/2*((0-xr)/vr)^2 < 0|0 < xo+Vmin()*(0-xr)/vr))`}, 1) ; <(
QE,
QE,
composeb(1) ; composeb(1.1) ; solve(1.1.1) ; chase(1) ; allR(1) ; implyR(1) ; andL(-1) ; andL(-7) ; andR(1) ; <(
implyR(1) ; allR(1) ; implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; orL(-9) ; <(
fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; hideR(2) ; QE
)
),
fullSimplify ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; hideR(3) ; hideR(1) ; QE
)
)
),
implyR(1) ; andR(1) ; <(
implyR(1) ; andL(-10) ; fullSimplify ; allR(1) ; implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; hideL(-7) ; hideR(3) ; andR(3) ; <(
QE,
orR(3) ; orL(-9) ; <(
hideR(4) ; hideL(-7) ; hideR(2) ; QE,
hideL(-7) ; hideR(3) ; hideR(2) ; QE
)
)
)
),
implyR(1) ; andR(1) ; <(
implyR(1) ; andL(-11) ; fullSimplify ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; orR(4) ; hideR(4) ; hideR(3) ; hideL(-7) ; hideL(-7) ; hideL(-7) ; QE
),
implyR(1) ; andR(1) ; <(
notOr(-9) ; andL(-9) ; notAnd(-9) ; notAnd(-10) ; fullSimplify ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; orL(-8) ; <(
hideR(4) ; hideR(1) ; hideR(1) ; hideL(-9) ; hideL(-9) ; QE,
andL(-8) ; fullSimplify ; fullSimplify ; closeFalse
)
)
),
andR(1) ; <(
implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; fullSimplify ; andR(1) ; <(
QE,
QE
),
implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; hideL(-10) ; hideL(-10) ; hideL(-9) ; hideL(-8) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
orR(1) ; orR(2) ; orR(3) ; hideR(4) ; hideR(1) ; hideR(1) ; QE
)
)
)
)
)
)
)
),
andL('L)* ; useAt({`<*> merge`}, {`1`}, 1) ; con({`v`}, {`A()>0&b()>0&ep()>0&Vmin()>0&vo>=Vmin()&vr>=0&(xo>0|vr=0)&xo+v*ep()*Vmin()>0`}, 1) ; <(
QE,
andL('L)* ; edit({`xo>0`}, -9) ; hideL(-1) ; fullSimplify ; iterated(1) ; orR(1) ; composed(2) ; composed(2) ; randomd(2) ; existsR({`0`}, 2) ; testd(2) ; andR(2) ; <(
QE,
composed(2) ; composed(2) ; choiced(2) ; orR(2) ; hideR(3) ; composed(2) ; testd(2) ; simplify(2) ; composed(2) ; randomd(2) ; existsR({`A()`}, 2) ; testd(2) ; andR(2) ; <(
QE,
assignd(2) ; solve(2) ; existsR({`ep()`}, 2) ; simplify(2) ; andR(2) ; <(
QE,
existsR({`vo_1+0`}, 2) ; fullSimplify ; existsR({`A()*ep()+vr_1`}, 2) ; simplify(2) ; existsR({`vo_1*ep()+xo_1`}, 2) ; simplify(2) ;
existsR({`A()*(ep()^2/2)+vr_1*ep()+xr_1`}, 2) ; simplify(2) ; edit({`vr>=A()*ep()`}, -11=={`vr=A()*ep()+vr_1`}) ; edit({`xr>=xr_1`}, -13=={`xr=A()*(ep()^2/2)+vr_1*ep()+xr_1`}) ; edit({`xo>0`}, -12=={`xo=vo_1*ep()+xo_1`}) ; hideL(-5=={`xo_1>0`}) ; hideL(-6=={`vr_1>=0`}) ;
con({`w`}, {`A()>0&b()>0&ep()>0&Vmin()>0&vo>=Vmin()&xo>0&vr>=A()*ep()&xr+w*ep()*(A()*ep())>0`}, 2) ; <(
QE,
QE,
andL('L)* ; composed(1) ; composed(1) ; randomd(1) ; existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
composed(1) ; solve(1.1) ; composed(1) ; choiced(1) ; orR(1) ; composed(1) ; testd(1) ; simplify(1) ; hideR(2) ; composed(1) ; randomd(1) ; existsR({`A()`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; simplify(1) ; QE
)
)
)
)
)
)
,
andL('L)* ; composed(1) ; composed(1) ; randomd(1) ; existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
composed(1) ; solve(1.1) ; composed(1) ; choiced(1) ; orR(1) ; orL(-12=={`xo>0|vr=0`}) ; <(
hideR(2) ; composed(1) ; testd(1) ; simplify(1) ; composed(1) ; randomd(1) ; existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; simplify(1) ; QE
),
composed(1) ; testd(1) ; andR(1) ; <(
composed(2) ; testd(2) ; andR(2) ; <(
QE,
choiced(2) ; orR(2) ; hideR(2) ; composed(2) ; testd(2) ; simplify(2) ; choiced(2) ; orR(2) ; hideR(2) ; composed(2) ; testd(2) ; simplify(2) ; choiced(2) ; orR(2) ; hideR(2) ; choiced(2) ; orR(2) ; hideR(3) ; composed(2) ; testd(2) ; simplify(2) ; assignd(2) ; assignd(2) ; existsR({`ep()`}, 2) ; simplify(2) ; QE
),
hideR(2) ; composed(1) ; randomd(1) ; existsR({`0`}, 1) ; testd(1) ; andR(1) ; <(
QE,
assignd(1) ; existsR({`ep()`}, 1) ; simplify(1) ; QE
)
)
)
)
)
)
End.
End.
Theorem "Theorem 13: Passive safety with trajectory distance measurement".
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R W(). /* maximum steering */
R V(). /* maximum obstacle velocity */
R abs(R). /* predefined function of absolute value */
R stopDist(R v) = (v^2 / (2*b()) + V()*v/b()).
R accelComp(R v, R a) = ((a/b() + 1) * (a/2 * ep()^2 + ep()*(v+V))).
R admissibleSeparationG(R v, R a) = (stopDist(v) + accelComp(v,a)).
R admissibleSeparationL(R v, R a) = (-v^2/(2*a)-V*v/a).
R trajectoryDist(R r, R xo, R xc, R yo, R yc) = ( abs(abs(r) - ((xo-xc)^2 + (yo-yc)^2)^(1/2)) ).
B isWellformedDir() <-> ( r!=0 & r^2 = (x-xc)^2 + (y-yc)^2 & dx^2 + dy^2 = 1 & dx = -(y-yc)/r & dy = (x-xc)/r & w*r=v ).
B bounds() <-> ( /* Bounds for global constants */
A() >= 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& V() >= 0
).
B initialState() <-> ( /* Stopped somewhere safe initially */
v = 0
& (x-xo)^2 + (y-yo)^2 > 0
& isWellformedDir()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> ( /* Conditions that are true on each loop iteration */
v >= 0
& isWellformedDir()
& (v>0 -> abs(x-xo) > stopDist(v) | abs(y-yo) > stopDist(v) | abs(abs(r) - ((xo-xc)^2 + (yo-yc)^2)^(1/2)) > V*v/b)
).
End.
ProgramVariables.
R x. /* robot position: x */
R y. /* robot position: y */
R v. /* robot translational velocity */
R a. /* robot translational acceleration */
R dx. /* robot orientation: x */
R dy. /* robot orientation: y */
R w. /* robot rotational velocity */
R r. /* robot curve radius */
R xc.
R yc.
R xo. /* position of closest obstacle on curve */
R yo.
R vxo. /* velocity vector of obstacle */
R vyo.
R t. /* time */
End.
Problem.
assumptions() ->
[
{
{
/* obstacle control */
{
vxo := *; vyo := *;
?vxo^2+vyo^2<=V^2;
}
/* robot control */
{
/* brake on current curve or remain stopped */
{ a := -b; }
++
{ ?v = 0; a := 0; w := 0; { dx:=-dx;dy:=-dy; ++ dx:=dx;dy:=dy; }; r := *; xc := *; yc := *;
?(r!=0 & r^2 = (x-xc)^2+(y-yc)^2 & dx=-(y-yc)/r & dy=(x-xc)/r & r*w=v); }
++
/* or choose a new safe curve */
{ a := *; ?-b<=a & a<=A;
w := *; ?-W<=w & w<=W; /* choose steering */
r := *;
xc := *; yc := *;
xo := *; yo := *; /* measure closest obstacle on the curve */
/* admissible curve */
?(r!=0 & r^2 = (x-xc)^2+(y-yc)^2 & dx=-(y-yc)/r & dy=(x-xc)/r & r*w=v);
/* use that curve, if it is a safe one (admissible velocities) */
if (v+a*ep>=0) { ?abs(x-xo) > admissibleSeparationG(v,a) | abs(y-yo) > admissibleSeparationG(v,a) | trajectoryDist(r,xo,xc,yo,yc) > V*(ep + (v+a*ep)/b); }
else { ?abs(x-xo) > admissibleSeparationL(v,a) | abs(y-yo) > admissibleSeparationL(v,a) | trajectoryDist(r,xo,xc,yo,yc) > -V*v/a; }
}
};
t := 0;
}
/* dynamics */
{ x' = v * dx, y' = v * dy, v' = a, /* accelerate/decelerate and move */
dx' = -w * dy, dy' = w * dx, w' = a/r, /* follow curve */
xo' = vxo, yo' = vyo, /* obstacle moves */
t' = 1 & t <= ep & v >= 0
}
}*@invariant(loopinv())
](v>0 -> (x - xo)^2 + (y - yo)^2 > 0)
End.
Tactic "Proof Theorem 13: Passive safety with trajectory distance measurement".
tactic dIHide as (
hideL('L~={`v>0->abs(x-xo)>v^2/(2*b())+V()*v/b()|abs(y-yo)>v^2/(2*b())+V()*v/b()|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`})
);
/* Some of the QE need QE({`Mathematica`}) */
implyR(1) ; loop({`v>=0&(r!=0&r^2=(x-xc)^2+(y-yc)^2&dx^2+dy^2=1&dx=-(y-yc)/r&dy=(x-xc)/r&w*r=v)&(v>0->abs(x-xo)>v^2/(2*b())+V()*v/b()|abs(y-yo)>v^2/(2*b())+V()*v/b()|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b())`}, 1) ; <(
print({`Base Case`}); QE; print({`Base Case Done`}),
print({`Use Case`}); unfold ; fullSimplify ; hideL('L=={`w*r=v`}) ; hideL('L=={`dy=(x-xc)/r`}) ; hideL('L=={`dx=-(y-yc)/r`}) ; hideL('L=={`dx^2+dy^2=1`}) ; hideL('L=={`ep()>0`}) ; orL(-5) ; <(
hideL('L=={`r^2=(x-xc)^2+(y-yc)^2`}) ; hideL('L=={`r!=0`}) ; QE,
orL(-5) ; <(
hideL('L=={`r^2=(x-xc)^2+(y-yc)^2`}) ; hideL('L=={`r!=0`}) ; QE,
edit({`expand(abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2)))>V()*v/b()`}, -5) ; edit({`expand(abs(r))-((xo-xc)^2+(yo-yc)^2)^(1/2)>=0&abs_0=abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2)|abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2) < 0&abs_0=-(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))`}, -8) ; orL(-9) ; <(
QE,
QE
)
)
); print({`Use Case Done`}),
unfold ; <(
print({`Induction Step (1)`});
dC({`t>=0&dx^2+dy^2=1&v=old(v)-b()*t&w*r=v`}, 1) ; <(
dC({`dx=-(y-yc)/r&dy=(x-xc)/r`}, 1) ; <(
dC({`xo=old(xo)+vxo*t&yo=old(yo)+vyo*t`}, 1) ; <(
dC({`-t*(v+b()/2*t)<=x-old(x)&x-old(x)<=t*(v+b()/2*t)`}, 1) ; <(
dC({`-t*(v+b()/2*t)<=y-old(y)&y-old(y)<=t*(v+b()/2*t)`}, 1) ; <(
print({`Induction Step (1) Differential Invariants Established`});
dW(1) ; implyR(1) ; andL('L)* ; fullSimplify ; andR(1) ; <(
hideL('L=={`v_0>0->abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()|abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*v_0/b()`}) ; QE,
implyR(1) ; orR(1) ; orR(2) ; hideL('L=={`A()>=0`}) ; hideL('L=={`ep()>0`}) ; hideL('L=={`t<=ep()`}) ; hideL('L=={`dx^2+dy^2=1`}) ; hideL('L=={`dy=(x-xc)/r`}) ; hideL('L=={`dx=-(y-yc)/r`}) ; hideL('L=={`dy_0=(x_0-xc)/r`}) ; hideL('L=={`dx_0=-(y_0-yc)/r`}) ; hideL('L=={`dx_0^2+dy_0^2=1`}) ; implyL(-6) ; <(
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ; QE,
orL(-6) ; <(
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; smartQE,
orL(-6) ; <(
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ; smartQE,
hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ;
edit({`abs(abs(r)-abbrv((((xo_0-xc)^2+(yo_0-yc)^2)^(1/2),oldCDist)))>V()*v_0/b()`}, 'L=={`abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*v_0/b()`}) ;
edit({`abs(abs(r)-abbrv((((xo-xc)^2+(yo-yc)^2)^(1/2),cDist)))>V()*v/b()`}, 'R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ;
cut({`abs(cDist-oldCDist)<=t*V()`}) ; <(
hideL('L=={`cDist=((xo-xc)^2+(yo-yc)^2)^(1/2)`}) ; hideL('L=={`oldCDist=((xo_0-xc)^2+(yo_0-yc)^2)^(1/2)`}) ; hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`}) ; hideL('L=={`w_0*r=v_0`}) ; hideL('L=={`vxo^2+vyo^2<=V()^2`}) ; smartQE,
hideR('R=={`abs(abs(r)-cDist)>V()*v/b()`}) ; hideL('L=={`abs(abs(r)-oldCDist)>V()*v_0/b()`}) ; hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`}) ; hideL('L=={`w_0*r=v_0`}) ; hideL('L=={`r!=0`}) ; hideL('L=={`v_0>=0`}) ; hideL('L=={`w*r=v`}) ; cut({`abs(cDist-oldCDist)<=t*(vxo^2+vyo^2)^(1/2)`}) ; <(
hideL('L=={`cDist=((xo-xc)^2+(yo-yc)^2)^(1/2)`}) ; hideL('L=={`oldCDist=((xo_0-xc)^2+(yo_0-yc)^2)^(1/2)`}) ; smartQE,
hideR('R=={`abs(cDist-oldCDist)<=t*V()`}) ; hideL('L=={`vxo^2+vyo^2<=V()^2`}) ; hideL('L=={`V()>=0`}) ; hideL('L=={`t_0=0`}) ; hideL('L=={`-t*(v+b()/2*t)<=y-y_0`}) ; hideL('L=={`y-y_0<=t*(v+b()/2*t)`}) ; hideL('L=={`-t*(v+b()/2*t)<=x-x_0`}) ; hideL('L=={`x-x_0<=t*(v+b()/2*t)`}) ; smartQE
)
)
)
)
)
),
dIHide ; dI(1)
),
dIHide ; dI(1)
),
dIHide ; dI(1)
),
dIHide ; dI(1)
),
dIHide ; dI(1)
); print({`Induction Step (1) Done`}),
print({`Induction Step (2)`});
dC({`t>=0&dx^2+dy^2=1&v=old(v)&w*r=v`}, 1) ; <(
dC({`dx=-(y-yc)/r&dy=(x-xc)/r`}, 1) ; <(
print({`Induction Step (2) Differential Invariants Established`});
dW(1) ; implyR(1) ; andL('L)* ; fullSimplify ; prop ; doall(smartQE),
dIHide ; dI(1)
),
dIHide ; dI(1)
); print({`Induction Step (2) Done`}),
print({`Induction Step (3)`});
dIHide ; hideL('L=={`r_0!=0`}) ; hideL('L=={`r_0^2=(x-xc_0)^2+(y-yc_0)^2`}) ; hideL('L=={`dx=-(y-yc_0)/r_0`}) ; hideL('L=={`dy=(x-xc_0)/r_0`}) ; hideL('L=={`w_0*r_0=v`}) ; dC({`t>=0&dx^2+dy^2=1&v=old(v)+a*t&w*r=v`}, 1) ; <(
dC({`dx=-(y-yc)/r&dy=(x-xc)/r`}, 1) ; <(
dC({`xo=old(xo)+vxo*t&yo=old(yo)+vyo*t`}, 1) ; <(
dC({`-t*(v-a/2*t)<=x-old(x)&x-old(x)<=t*(v-a/2*t)`}, 1) ; <(
dC({`-t*(v-a/2*t)<=y-old(y)&y-old(y)<=t*(v-a/2*t)`}, 1) ; <(
print({`Induction Step (3) Differential Invariants Established`});
dW(1) ; implyR(1) ; andL('L)* ; fullSimplify ; hideL('L=={`-W()<=w_0`}) ; hideL('L=={`w_0<=W()`}) ; andR(1) ; <(
hideL('L=={`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; QE,
implyR(1) ; orR(1) ; orR(2) ; hideL('L~={`dx^2+dy^2=1`})*2 ; hideL('L~={`dy=(x-xc)/r`})*2 ; hideL('L~={`dx=-(y-yc)/r`})*2 ; hideL('L=={`t_0=0`}) ;
orL('L=={`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; <(
edit({`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*t^2+t*(v_0+V()))`}, 'L=={`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))`}) ;
hideL('L=={`v_0+a*ep()>=0`}) ; hideL('L=={`t<=ep()`}) ; hideL('L=={`ep()>0`}) ;
hideL('L=={`w*r=v`}); hideL('L=={`r*w_0=v_0`}); hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`});
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; smartQE,
orL('L=={`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; <(
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ;
edit({`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*t^2+t*(v_0+V()))`}, 'L=={`abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))`}) ;
hideL('L=={`v_0+a*ep()>=0`}) ; hideL('L=={`ep()>0`}) ; hideL('L=={`t<=ep()`}) ;
hideL('L=={`w*r=v`}); hideL('L=={`r*w_0=v_0`}); hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`});
smartQE
,
hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ;
edit({`abs(abs(r)-abbrv((((xo_0-xc)^2+(yo_0-yc)^2)^(1/2),oldCDist)))>V()*(ep()+(v_0+a*ep())/b())`}, 'L=={`abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ;
edit({`abs(abs(r)-abbrv((((xo-xc)^2+(yo-yc)^2)^(1/2),cDist)))>V()*v/b()`}, 'R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ;
hideL('L=={`r!=0`}) ; hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`}) ; hideL('L=={`r*w_0=v_0`}) ; hideL('L=={`v_0+a*ep()>=0`}) ; cut({`abs(cDist-oldCDist)<=t*V()`}) ; <(
hideL('L=={`oldCDist=((xo_0-xc)^2+(yo_0-yc)^2)^(1/2)`}) ; hideL('L=={`cDist=((xo-xc)^2+(yo-yc)^2)^(1/2)`}) ;
edit({`abs(abs(r)-oldCDist)>V()*(t+(v_0+a*t)/b())`}, 'L=={`abs(abs(r)-oldCDist)>V()*(ep()+(v_0+a*ep())/b())`}) ;
hideL('L=={`ep()>0`}) ; hideL('L=={`t<=ep()`}) ; smartQE
,
hideR('R=={`abs(abs(r)-cDist)>V()*v/b()`}) ; hideL('L=={`abs(abs(r)-oldCDist)>V()*(ep()+(v_0+a*ep())/b())`}) ; hideL('L=={`t<=ep()`}) ; hideL('L=={`ep()>0`}) ; cut({`abs(cDist-oldCDist)<=t*(vxo^2+vyo^2)^(1/2)`}) ; <(
hideL('L=={`oldCDist=((xo_0-xc)^2+(yo_0-yc)^2)^(1/2)`}) ; hideL('L=={`cDist=((xo-xc)^2+(yo-yc)^2)^(1/2)`}) ;
edit({`abbrv((abs(cDist-oldCDist),X))<=t*V()`}, 'R=={`abs(cDist-oldCDist)<=t*V()`}) ;
hideL('L=={`X=abs(cDist-oldCDist)`}) ; hideL('L=={`A()>=0`}) ; hideL('L=={`-b()<=a`}) ; hideL('L=={`a<=A()`}) ; hideL('L=={`-t*(v-a/2*t)<=y-y_0`}) ; hideL('L=={`y-y_0<=t*(v-a/2*t)`}) ; hideL('L=={`-t*(v-a/2*t)<=x-x_0`}) ; hideL('L=={`x-x_0<=t*(v-a/2*t)`}) ; hideL('L=={`xo=xo_0+vxo*t`}) ; hideL('L=={`yo=yo_0+vyo*t`}) ; hideL('L=={`v=v_0+a*t`}) ; hideL('L=={`v>=0`}) ; hideL('L=={`w*r=v`}) ; hideL('L=={`v>0`}) ; hideL('L=={`b()>0`}) ; QE,
hideR('R=={`abs(cDist-oldCDist)<=t*V()`}) ; hideL('L=={`vxo^2+vyo^2<=V()^2`}) ; hideL('L=={`V()>=0`}) ; hideL('L=={`w*r=v`}) ; hideL('L=={`a<=A()`}) ; hideL('L=={`A()>=0`}) ; hideL('L=={`-t*(v-a/2*t)<=y-y_0`}) ; hideL('L=={`y-y_0<=t*(v-a/2*t)`}) ; hideL('L=={`-t*(v-a/2*t)<=x-x_0`}) ; hideL('L=={`x-x_0<=t*(v-a/2*t)`}) ; hideL('L=={`v=v_0+a*t`}) ; hideL('L=={`v>0`}) ; hideL('L=={`v>=0`}) ; hideL('L=={`-b()<=a`}) ; hideL('L=={`b()>0`}) ; smartQE
)
)
)
)
),
hideL('L=={`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y_0-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; dI(1)
),
hideL('L=={`abs(x_0-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; dI(1)
),
hideL('L=={`abs(x-xo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y-yo_0)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; dI(1)
),
hideL('L=={`abs(x-xo)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y-yo)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; dI(1)
),
hideL('L=={`abs(x-xo)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(y-yo)>v_0^2/(2*b())+V()*v_0/b()+(a/b()+1)*(a/2*ep()^2+ep()*(v_0+V()))|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*(ep()+(v_0+a*ep())/b())`}) ; dI(1)
); print({`Induction Step (3) Done`}),
print({`Induction Step (4)`});
dC({`t>=0&dx^2+dy^2=1&v=old(v)&w*r=v`}, 1) ; <(
dC({`dx=-(y-yc)/r&dy=(x-xc)/r`}, 1) ; <(
print({`Induction Step (4) Differential Invariants Established`});
dW(1) ; implyR(1) ; andL('L)* ; fullSimplify;
andR(1); <(
QE
,
hideL('L=={`w*r=v`}); hideL('L=={`dx^2+dy^2=1`});
hideL('L=={`dy=(x-xc)/r`}); hideL('L=={`dx=-(y-yc)/r`});
hideL('L=={`w_1*r_0=v_0`}); hideL('L=={`dy_0=(x_0-xc_0)/r_0`}); hideL('L=={`dx_0^2+dy_0^2=1`});
hideL('L=={`dx_0=-(y_0-yc_0)/r_0`}); hideL('L=={`r_0^2=(x_0-xc_0)^2+(y_0-yc_0)^2`});
hideL('L=={`r_0!=0`}); hideL('L=={`r*w_0=v_0`});
hideL('L=={`dy_0=(x_0-xc)/r`}); hideL('L=={`dx_0=-(y_0-yc)/r`});
hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`}); hideL('L=={`r!=0`}); hideL('L=={`w_0=0`});
smartQE
)
,
hideL('L=={`v_0>0->abs(x-xo)>v_0^2/(2*b())+V()*v_0/b()|abs(y-yo)>v_0^2/(2*b())+V()*v_0/b()|abs(abs(r_0)-((xo-xc_0)^2+(yo-yc_0)^2)^(1/2))>V()*v_0/b()`}) ; dI(1)
),
hideL('L=={`v_0>0->abs(x-xo)>v_0^2/(2*b())+V()*v_0/b()|abs(y-yo)>v_0^2/(2*b())+V()*v_0/b()|abs(abs(r_0)-((xo-xc_0)^2+(yo-yc_0)^2)^(1/2))>V()*v_0/b()`}) ; dI(1)
); print({`Induction Step (4) Done`}),
print({`Induction Step (5)`});
hideL('L=={`v>0->abs(x-xo_0)>v^2/(2*b())+V()*v/b()|abs(y-yo_0)>v^2/(2*b())+V()*v/b()|abs(abs(r_0)-((xo_0-xc_0)^2+(yo_0-yc_0)^2)^(1/2))>V()*v/b()`}) ; hideL('L=={`r_0!=0`}) ; hideL('L=={`r_0^2=(x-xc_0)^2+(y-yc_0)^2`}) ; hideL('L=={`dx=-(y-yc_0)/r_0`}) ; hideL('L=={`dy=(x-xc_0)/r_0`}) ; hideL('L=={`w_0*r_0=v`}) ; hideL('L=={`-W()<=w`}) ; hideL('L=={`w<=W()`}) ; cut({`a < 0`}) ; <(
hideL('L=={`a<=A()`}) ; hideL('L=={`A()>=0`}) ; dC({`t>=0&dx^2+dy^2=1&v=old(v)+a*t&w*r=v`}, 1) ; <(
dC({`dx=-(y-yc)/r&dy=(x-xc)/r`}, 1) ; <(
dC({`xo=old(xo)+vxo*t&yo=old(yo)+vyo*t`}, 1) ; <(
dC({`-t*(v-a/2*t)<=x-old(x)&x-old(x)<=t*(v-a/2*t)`}, 1) ; <(
dC({`-t*(v-a/2*t)<=y-old(y)&y-old(y)<=t*(v-a/2*t)`}, 1) ; <(
print({`Induction Step (5) Differential Invariants Established`});
dW(1) ; implyR(1) ; andL('L)* ; fullSimplify ; andR(1) ; <(
hideL('L=={`abs(x_0-xo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(y_0-yo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ; QE,
implyR(1) ; orR(1) ; orR(2) ; hideL('L=={`dx^2+dy^2=1`}) ; hideL('L=={`dy=(x-xc)/r`}) ; hideL('L=={`dx=-(y-yc)/r`}) ; hideL('L=={`dy_0=(x_0-xc)/r`}) ; hideL('L=={`dx_0=-(y_0-yc)/r`}) ; hideL('L=={`dx_0^2+dy_0^2=1`}) ;
orL('L=={`abs(x_0-xo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(y_0-yo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ; <(
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; smartQE,
orL('L=={`abs(y_0-yo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ; <(
hideR('R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ; smartQE,
hideR('R=={`abs(y-yo)>v^2/(2*b())+V()*v/b()`}) ; hideR('R=={`abs(x-xo)>v^2/(2*b())+V()*v/b()`}) ;
edit({`abs(abs(r)-abbrv((((xo_0-xc)^2+(yo_0-yc)^2)^(1/2),oldCDist)))>-V()*v_0/a`}, 'L=={`abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ;
edit({`abs(abs(r)-abbrv((((xo-xc)^2+(yo-yc)^2)^(1/2),cDist)))>V()*v/b()`}, 'R=={`abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()`}) ;
cut({`abs(cDist-oldCDist)<=t*V()`}) ; <(
hideL('L=={`cDist=((xo-xc)^2+(yo-yc)^2)^(1/2)`}) ; hideL('L=={`oldCDist=((xo_0-xc)^2+(yo_0-yc)^2)^(1/2)`}) ; smartQE,
hideR('R=={`abs(abs(r)-cDist)>V()*v/b()`}) ; hideL('L=={`-t*(v-a/2*t)<=y-y_0`}) ; hideL('L=={`y-y_0<=t*(v-a/2*t)`}) ; hideL('L=={`-t*(v-a/2*t)<=x-x_0`}) ; hideL('L=={`x-x_0<=t*(v-a/2*t)`}) ; hideL('L=={`v=v_0+a*t`}) ; hideL('L=={`w*r=v`}) ; hideL('L=={`v>0`}) ; hideL('L=={`v>=0`}) ; hideL('L=={`t<=ep()`}) ; hideL('L=={`ep()>0`}) ; hideL('L=={`r!=0`}) ; hideL('L=={`r^2=(x_0-xc)^2+(y_0-yc)^2`}) ; hideL('L=={`t_0=0`}) ; hideL('L=={`r*w_0=v_0`}) ; hideL('L=={`-b()<=a`}) ; hideL('L=={`b()>0`}) ; cut({`abs(cDist-oldCDist)<=t*(vxo^2+vyo^2)^(1/2)`}) ; <(
hideL('L=={`oldCDist=((xo_0-xc)^2+(yo_0-yc)^2)^(1/2)`}) ; hideL('L=={`cDist=((xo-xc)^2+(yo-yc)^2)^(1/2)`}) ;
edit({`abbrv((abs(cDist-oldCDist),X))<=t*V()`}, 'R=={`abs(cDist-oldCDist)<=t*V()`}) ;
hideL('L=={`X=abs(cDist-oldCDist)`}) ; hideL('L=={`abs(abs(r)-oldCDist)>-V()*v_0/a`}) ; QE,
hideR('R=={`abs(cDist-oldCDist)<=t*V()`}) ; hideL('L=={`vxo^2+vyo^2<=V()^2`}) ;
hideL('L=={`abs(abs(r)-oldCDist)>-V()*v_0/a`}) ; hideL('L=={`a < 0`}) ; hideL('L=={`V()>=0`}) ; hideL('L=={`v_0>=0`});
smartQE
)
)
)
)
),
hideL('L=={`abs(x_0-xo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(y_0-yo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ; dI(1)
),
hideL('L=={`abs(x_0-xo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(y-yo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ; dI(1)
),
hideL('L=={`abs(x-xo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(y-yo_0)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo_0-xc)^2+(yo_0-yc)^2)^(1/2))>-V()*v_0/a`}) ; dI(1)
),
hideL('L=={`abs(x-xo)>-v_0^2/(2*a)-V()*v_0/a|abs(y-yo)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>-V()*v_0/a`}) ; dI(1)
),
hideL('L=={`abs(x-xo)>-v_0^2/(2*a)-V()*v_0/a|abs(y-yo)>-v_0^2/(2*a)-V()*v_0/a|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>-V()*v_0/a`}) ; dI(1)
),
hideR('R=={`[{x'=v*dx,y'=v*dy,v'=a,dx'=-w*dy,dy'=w*dx,w'=a/r,xo'=vxo,yo'=vyo,t'=1&t<=ep()&v>=0}](v>=0&(r!=0&r^2=(x-xc)^2+(y-yc)^2&dx^2+dy^2=1&dx=-(y-yc)/r&dy=(x-xc)/r&w*r=v)&(v>0->abs(x-xo)>v^2/(2*b())+V()*v/b()|abs(y-yo)>v^2/(2*b())+V()*v/b()|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>V()*v/b()))`}) ; hideL('L=={`abs(x-xo)>-v^2/(2*a)-V()*v/a|abs(y-yo)>-v^2/(2*a)-V()*v/a|abs(abs(r)-((xo-xc)^2+(yo-yc)^2)^(1/2))>-V()*v/a`}) ; QE
)
); print({`Induction Step (5) Done`})
); print({`Proof Done`})
End.
End.
Theorem "Theorem 14: Reach waypoint with deadline".
/*
* Robot must stop within distance delta at goal.
*
* Robot
* - must stop within distance delta of goal
* - can only drive straight and forward
* - ensures progress towards goal
*
* Liveness property:
* - Robot can stop at goal
*
*/
Functions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R GDelta(). /* goal area size */
R Vmax(). /* robot cannot go faster than this */
R waypointStartDist(R xg) = ( xg-GDelta() ).
R waypointEndDist(R xg) = ( xg+GDelta() ).
R minV() = ( A()*ep() ).
R maxTravelTime(R g) = ( waypointStartDist(g)/minV() ).
R stopTime(R v) = ( v/b() ).
R speedUpTime(R v) = ( ep()-v/A() ).
R stopDist(R v) = ( v^2/(2*b()) ).
R accComp(R v) = ( (A()/b() + 1)*(A()/2*ep()^2 + ep()*v) ).
B bounds() <-> ( /* Bounds for global constants */
A() > 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& Vmax() >= 2*A()*ep()
& GDelta() > Vmax()*ep() + Vmax()^2/(2*b()) /* waypoint is large enough that robot can
start driving and still stop inside */
& T > ep() + maxTravelTime(xg-xr) + ep() + stopTime(Vmax())
).
B initialState() <-> ( /* Stopped somewhere safe initially */
vr = 0
& xr < waypointStartDist(xg)
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B loopinv() <-> (
0 <= vr & vr <= Vmax & xr + stopDist(vr) < waypointEndDist(xg)
& (waypointStartDist(xg) < xr -> (vr = 0 | T >= stopTime(vr)))
& (xr <= waypointStartDist(xg) ->
(vr >= minV() & T > maxTravelTime(xg-xr) + ep() + stopTime(Vmax()))
| (vr <= minV() & T > speedUpTime(vr) + maxTravelTime(xg-xr) + ep() + stopTime(Vmax())))
).
HP ctrl ::= {
if (xr > waypointStartDist(xg)) {
/* in the goal area: brake or stay stopped */
ar := -b(); ++ ?vr = 0; ar := 0;
} else {
if (xr + stopDist(vr) + accComp(vr) < waypointEndDist(xg) & vr+A()*ep() <= Vmax()) {
/* if robot can stop from higher speed before leaving goal area then accelerate */
ar := A();
} else {
/* else coast until at goal */
ar := 0;
}
}
}.
HP dyn ::= { {xr' = vr, vr' = ar, t' = 1, T'=-1 & t <= ep() & vr >= 0} }.
HP dwwpdl ::= {
{ { ctrl; t := 0; }
dyn;
}*@invariant(loopinv())
}.
End.
ProgramVariables.
R xr. /* robot position: x */
R vr. /* robot translational velocity */
R ar. /* robot translational acceleration */
R xg. /* goal position */
R t. /* control cycle time */
R T. /* global time */
End.
Problem.
assumptions()
-> [ dwwpdl; ](xr < waypointEndDist(xg) & (T <= 0 -> (waypointStartDist(xg) < xr & vr = 0)))
& < dwwpdl; >(waypointStartDist(xg) < xr & vr = 0)
End.
Tactic "Proof Theorem 14: Reach waypoint with deadline".
/* Some of the QE need QE({`Mathematica`}) */
implyR(1) ; andR(1) ; <(
loop({`0<=vr&vr<=Vmax()&xr+vr^2/(2*b()) < xg+GDelta()&(xg-GDelta() < xr->vr=0|T>=vr/b())&(xr<=xg-GDelta()->vr>=A()*ep()&T>(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()|vr<=A()*ep()&T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b())`}, 1) ; <(
QE,
andR(1) ; <(
andL('L)* ; hideL('L=={`xr<=xg-GDelta()->vr>=A()*ep()&T>(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()|vr<=A()*ep()&T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; QE,
implyR(1) ; andL('L)* ; andR(1) ; <(
hideL('L=={`xg-GDelta() < xr->vr=0|T>=vr/b()`}) ; implyL(-10) ; <(
QE,
QE
),
implyL(-10) ; <(
implyL(-10) ; <(
QE,
QE
),
hideL('L=={`xr<=xg-GDelta()->vr>=A()*ep()&T>(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()|vr<=A()*ep()&T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; QE
)
)
),
andL('L)* ; notGreater(1.0.0.0.1.0.0) ; notAnd(1.0.0.0.1.1.1.0.0) ; composeb(1) ; solve(1.1) ; chase(1) ; andR(1) ; <(
implyR(1) ; fullSimplify ; andR(1) ; <(
allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
andR(1) ; <(
QE,
andR(1) ; <(
QE,
implyR(1) ; orR(1) ; allL({`t_`}, -12) ; implyL(-12) ; <(
hideR('R=={`(-b())*t_+vr>=A()*ep()&-t_+T>(xg-((-b())*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideR('R=={`(-b())*t_+vr<=A()*ep()&-t_+T>ep()-((-b())*t_+vr)/A()+(xg-((-b())*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; QE,
hideR('R=={`(-b())*t_+vr>=A()*ep()&-t_+T>(xg-((-b())*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideR('R=={`(-b())*t_+vr<=A()*ep()&-t_+T>ep()-((-b())*t_+vr)/A()+(xg-((-b())*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideL('L=={`GDelta()>Vmax()*ep()+Vmax()^2/(2*b())`}) ; hideL('L=={`xr+vr^2/(2*b()) < xg+GDelta()`}) ; QE
)
)
)
)
),
implyR(1) ; fullSimplify ; allR(1) ; implyR(1) ; implyR(1) ; QE
),
implyR(1) ; fullSimplify ; andR(1) ; <(
implyR(1) ; andL(-11) ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
andR(1) ; <(
hideL('L=={`vr>=A()*ep()&T>(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()|vr<=A()*ep()&T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideL('L=={`xr<=xg-GDelta()`}) ; hideL('L=={`xr+vr^2/(2*b()) < xg+GDelta()`}) ; hideL('L=={`Vmax()>=2*A()*ep()`}) ; hideL('L=={`GDelta()>Vmax()*ep()+Vmax()^2/(2*b())`}) ; hideL('L=={`vr<=Vmax()`}) ; hideL('L=={`vr+A()*ep()<=Vmax()`}) ; QE,
andR(1) ; <(
hideL('L=={`xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()`}) ; hideL(-8=={`xr+vr^2/(2*b()) < xg+GDelta()`}) ; implyR(1) ; orR(1) ; QE,
implyR(1) ; orR(1) ; hideL('L=={`xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()`}) ; hideL('L=={`xr+vr^2/(2*b()) < xg+GDelta()`}) ; orL(-8) ; <(
hideR('R=={`A()*t_+vr<=A()*ep()&-t_+T>ep()-(A()*t_+vr)/A()+(xg-(A()*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; andL(-8) ; andR(1) ; <(
QE,
QE
),
andL(-8) ; andR(1) ; <(
andR(2) ; <(
QE,
QE
),
andR(2) ; <(
allL({`t_`}, -11) ; implyL(-11) ; <(
hideR('R=={`-t_+T>(xg-(A()*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideR('R=={`A()*t_+vr<=A()*ep()`}) ; QE,
andL(-11) ; hideL('L=={`A()*(t_^2/2)+vr*t_+xr<=xg-GDelta()`}) ; hideL('L=={`GDelta()>Vmax()*ep()+Vmax()^2/(2*b())`}) ; edit({`-t_+T>(xg-(A()*(t_^2/2)+vr*t_+xr)-GDelta())/(A()*ep())+abbrv(ep()+Vmax()/b())`}, 1) ; edit({`T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+abbrv`}, -11) ; hideL('L=={`abbrv=ep()+Vmax()/b()`}) ; edit({`vr+A()*t_<=Vmax()`}, -8) ; QE
),
QE
)
)
)
)
)
)
),
implyR(1) ; allR(1) ; implyR(1) ; implyR(1) ; andR(1) ; <(
hideL('L=={`vr>=A()*ep()&T>(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()|vr<=A()*ep()&T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideL('L=={`xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr)>=xg+GDelta()|vr+A()*ep()>Vmax()`}) ; QE,
andR(1) ; <(
hideL('L=={`xr+vr^2/(2*b()) < xg+GDelta()`}) ; allL({`t_`}, -12) ; implyL(-12) ; <(
hideR('R=={`xg-GDelta() < vr*t_+xr->vr=0|-t_+T>=vr/b()`}) ; QE,
orL(-8) ; <(
orL(-10) ; <(
QE,
QE
),
implyR(1) ; orR(1) ; orL(-10) ; <(
QE,
QE
)
)
),
implyR(1) ; orR(1) ; fullSimplify ; orL(-9) ; <(
hideR('R=={`vr<=A()*ep()&-t_+T>ep()-vr/A()+(xg-(vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; andL(-9) ; fullSimplify ; orL(-10) ; <(
edit({`-t_+T>(xg-(vr*t_+xr)-GDelta())/(A()*ep())+abbrv(ep()+Vmax()/b())`}, 1) ; edit({`T>(xg-xr-GDelta())/(A()*ep())+abbrv`}, -15) ; hideL('L=={`abbrv=ep()+Vmax()/b()`}) ; allL({`t_`}, -12) ; implyL(-12) ; <(
QE,
hideL('L=={`xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr)>=xg+GDelta()`}) ; hideL('L=={`GDelta()>Vmax()*ep()+Vmax()^2/(2*b())`}) ; QE
),
allL({`t_`}, -12) ; implyL(-12) ; <(
QE,
edit({`-t_+T>(xg-(vr*t_+xr)-GDelta())/(A()*ep())+abbrv(ep()+Vmax()/b())`}, 1) ; edit({`T>(xg-xr-GDelta())/(A()*ep())+abbrv`}, -15) ; hideL('L=={`abbrv=ep()+Vmax()/b()`}) ; hideL('L=={`xr+vr^2/(2*b()) < xg+GDelta()`}) ; hideL('L=={`GDelta()>Vmax()*ep()+Vmax()^2/(2*b())`}) ; QE
)
),
allL({`t_`}, -13) ; implyL(-13) ; <(
hideR('R=={`vr>=A()*ep()&-t_+T>(xg-(vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideR('R=={`vr<=A()*ep()&-t_+T>ep()-vr/A()+(xg-(vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; QE,
andL(-9) ; fullSimplify ; hideR(1=={`vr>=A()*ep()&-t_+T>(xg-(vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideR('R=={`-t_+T>ep()-vr/A()+(xg-(vr*t_+xr)-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; orL(-10) ; <(
hideL('L=={`T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; hideL('L=={`xr<=xg-GDelta()`}) ; QE,
hideL('L=={`T>ep()-vr/A()+(xg-xr-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ; QE
)
)
)
)
)
)
)
),
notGreater(1.0.0.0.0.1.0.0) ; notAnd(1.0.0.0.0.1.1.1.0.0) ; iterated(1) ; orR(1) ; composed(2) ; solve(2.1) ; composed(2) ; choiced(2) ; orR(2) ;
hideR('R=={`<?xr_1>xg-GDelta();{ar:=-b();++?vr_1=0;ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr_1>=0)&\exists T (T=-t_+T_1&\exists vr (vr=ar*t_+vr_1&\exists xr (xr=ar*(t_^2/2)+vr_1*t_+xr_1&<{{{?xr>xg-GDelta();{ar:=-b();++?vr=0;ar:=0;}++?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}}t:=0;}{xr'=vr,vr'=ar,t'=1,T'=-1&t<=ep()&vr>=0}}*>(xg-GDelta() < xr&vr=0)))))`}) ; composed(2) ; andL('L)* ; testd(2) ; hideL('L=={`T_1>ep()+(xg-xr_1-GDelta())/(A()*ep())+ep()+Vmax()/b()`}) ;
simplify(2) ; choiced(2) ; orR(2) ; composed(2) ; testd(2) ; andR(2) ; <(
hideR('R=={`<?!xr_1+vr_1^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr_1) < xg+GDelta()|!vr_1+A()*ep()<=Vmax();ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr_1>=0)&\exists T (T=-t_+T_1&\exists vr (vr=ar*t_+vr_1&\exists xr (xr=ar*(t_^2/2)+vr_1*t_+xr_1&<{{{?xr>xg-GDelta();{ar:=-b();++?vr=0;ar:=0;}++?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}}t:=0;}{xr'=vr,vr'=ar,t'=1,T'=-1&t<=ep()&vr>=0}}*>(xg-GDelta() < xr&vr=0)))))`}) ;
QE
,
hideR('R=={`<?!xr_1+vr_1^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr_1) < xg+GDelta()|!vr_1+A()*ep()<=Vmax();ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr_1>=0)&\exists T (T=-t_+T_1&\exists vr (vr=ar*t_+vr_1&\exists xr (xr=ar*(t_^2/2)+vr_1*t_+xr_1&<{{{?xr>xg-GDelta();{ar:=-b();++?vr=0;ar:=0;}++?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}}t:=0;}{xr'=vr,vr'=ar,t'=1,T'=-1&t<=ep()&vr>=0}}*>(xg-GDelta() < xr&vr=0)))))`}) ;
assignd(2) ; assignd(2) ; existsR({`ep()`}, 2) ; andR(2) ; <(
QE
,
andR(2) ; <(
QE
,
existsR({`-ep()+T_1`}, 2) ; simplify(2) ; existsR({`A()*ep()+vr_1`}, 2) ; simplify(2) ;
existsR({`A()*(ep()^2/2)+vr_1*ep()+xr_1`}, 2) ; simplify(2) ;
useAt({`<*> merge`}, {`1`}, 2) ; hideL(-8=={`T=-ep()+T_1`}) ;
print({`Outer convergence`});
con({`u`}, {`Vmax()>0&A()>0&b()>0&ep()>0&0 < vr&vr<=Vmax()&(xg-GDelta() < xr|xg-GDelta() < xr+u*ep()*vr)`}, 2) ; <(
QE,
andL('L)* ; edit({`xg-GDelta() < xr`}, -8) ; hideL('L=={`u<=0`}) ; useAt({`<*> merge`}, {`1`}, 1) ;
print({`Middle convergence`});
con({`v`}, {`Vmax()>0&A()>0&b()>0&ep()>0&vr>=0&vr-v*ep()*b()<=b()*ep()&xg-GDelta() < xr`}, 1) ; <(
QE
,
andL('L)* ; edit({`vr<=b()*ep()`}, -7) ; hideL('L=={`v<=0`}) ; iterated(1) ; orR(1) ; composed(2) ; solve(2.1) ;
composed(2) ; choiced(2) ; orR(2) ; composed(2) ; testd(2) ; simplify(2) ;
hideR('R=={`<?xr_2<=xg-GDelta();{?xr_2+vr_2^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr_2) < xg+GDelta()&vr_2+A()*ep()<=Vmax();ar:=A();++?!xr_2+vr_2^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr_2) < xg+GDelta()|!vr_2+A()*ep()<=Vmax();ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr_2>=0)&\exists T (T=-t_+T_1&\exists vr (vr=ar*t_+vr_2&\exists xr (xr=ar*(t_^2/2)+vr_2*t_+xr_2&<{{{?xr>xg-GDelta();{ar:=-b();++?vr=0;ar:=0;}++?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}}t:=0;}{xr'=vr,vr'=ar,t'=1,T'=-1&t<=ep()&vr>=0}}*>(xg-GDelta() < xr&vr=0)))))`}) ;
choiced(2) ; orR(2) ;
hideR('R=={`<?vr_2=0;ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr_2>=0)&\exists T (T=-t_+T_1&\exists vr (vr=ar*t_+vr_2&\exists xr (xr=ar*(t_^2/2)+vr_2*t_+xr_2&<{{{?xr>xg-GDelta();{ar:=-b();++?vr=0;ar:=0;}++?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}}t:=0;}{xr'=vr,vr'=ar,t'=1,T'=-1&t<=ep()&vr>=0}}*>(xg-GDelta() < xr&vr=0)))))`}) ;
assignd(2) ; assignd(2) ; existsR({`vr_2/b()`}, 2) ; andR(2) ; <(
QE,
andR(2) ; <(
QE,
existsR({`-vr_2/b()+T_1`}, 2) ; simplify(2) ; existsR({`0`}, 2) ; andR(2) ; <(
QE,
existsR({`vr_2^2/(2*b())+xr_2`}, 2) ; andR(2) ; <(
QE,
print({`Inner convergence`});
con({`w`}, {`Vmax()>0&A()>0&b()>0&ep()>0&vr=0&xg-GDelta() < xr`}, 2) ; <(
QE,
QE,
composed(1) ; solve(1.1) ; composed(1) ; andL('L)* ; choiced(1) ; orR(1) ;
hideR('R=={`<?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&ar*t_+vr=0&xg-GDelta() < ar*(t_^2/2)+vr*t_+xr)`}) ; composed(1) ; testd(1) ; simplify(1) ; choiced(1) ; orR(1) ; hideR(1=={`<ar:=-b();><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&ar*t_+vr=0&xg-GDelta() < ar*(t_^2/2)+vr*t_+xr)`}) ;
composed(1) ; testd(1) ; simplify(1) ; assignd(1) ; assignd(1) ; fullSimplify ; QE
);
print({`Inner convergence done`})
)
)
)
);
print({`Middle convergence done`})
,
andL('L)* ; composed(1) ; solve(1.1) ; composed(1) ; choiced(1) ; orR(1) ;
hideR('R=={`<?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&ar*t_+vr-(v-1)*ep()*b()<=b()*ep()&xg-GDelta() < ar*(t_^2/2)+vr*t_+xr)`}) ; composed(1) ; testd(1) ; simplify(1) ; choiced(1) ; orR(1) ; hideR(2=={`<?vr=0;ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&ar*t_+vr-(v-1)*ep()*b()<=b()*ep()&xg-GDelta() < ar*(t_^2/2)+vr*t_+xr)`}) ;
assignd(1) ; assignd(1) ; QE
);
print({`Outer convergence done`})
,
andL('L)* ; composed(1) ; solve(1.1) ; composed(1) ; choiced(1) ; orR(1) ; composed(1) ; testd(1) ;
hideL('L=={`ep()>0`}) ; hideL('L=={`b()>0`}) ; hideL('L=={`A()>0`}) ; orL('L=={`xg-GDelta() < xr|xg-GDelta() < xr+u*ep()*vr`}) ; <(
hideL('L=={`xr_1 < xg-GDelta()`}) ; hideL('L=={`vr_1=0`}) ;
simplify(1) ;
hideR('R=={`<?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr)))`}) ;
choiced(1) ; orR(1) ;
hideR('R=={`<?vr=0;ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr)))`}) ;
assignd(1) ; assignd(1) ;
existsR({`min(ep(),vr/b())/2`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; andR(1) ; doall(QE)
)
)
,
cut({`xr>xg-GDelta()&(xr>xg-GDelta()-><ar:=-b();++?vr=0;ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr))))`}) ; <(
hideR('R=={`<?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr)))`}) ;
andL('Llast) ; fullSimplify ; closeTrue
,
hideR('R=={`xr>xg-GDelta()&<ar:=-b();++?vr=0;ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr)))`}) ;
andR(2) ; <(
composed(1) ; testd(1) ; andR(1) ; <(
QE,
choiced(1) ; orR(1) ; composed(2) ; testd(2) ; andR(2) ; <(
composed(3) ; testd(3) ; andR(3) ; <(
prop,
assignd(3) ; assignd(3) ; existsR({`ep()`}, 3) ; fullSimplify ; QE
)
,
assignd(2) ; assignd(2) ; composed(3) ; testd(3) ; andR(3) ; <(
fullSimplify ; orR(3) ; existsR({`ep()`}, 2) ; andR(2) ; <(
QE,
andR(2) ; <(
QE,
andR(2) ; <(
QE,
andR(2) ; <(
QE,
orR(2) ; QE
)
)
)
)
,
assignd(3) ; assignd(3) ; existsR({`ep()`}, 3) ;
hideR('R=={`\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+0<=ep()&A()*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < A()*t_+vr&A()*t_+vr<=Vmax()&(xg-GDelta() < A()*(t_^2/2)+vr*t_+xr|xg-GDelta() < A()*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(A()*t_+vr)))`}) ;
fullSimplify ; QE
)
)
)
,
hideR('R=={`<?xr<=xg-GDelta();{?xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()&vr+A()*ep()<=Vmax();ar:=A();++?!xr+vr^2/(2*b())+(A()/b()+1)*(A()/2*ep()^2+ep()*vr) < xg+GDelta()|!vr+A()*ep()<=Vmax();ar:=0;}><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr)))`}) ;
implyR(1) ; choiced(1) ; orR(1) ;
hideR('R=={`<?vr=0;ar:=0;><t:=0;>\exists t_ (t_>=0&\forall s_ (0<=s_&s_<=t_->s_+t<=ep()&ar*s_+vr>=0)&Vmax()>0&A()>0&b()>0&ep()>0&0 < ar*t_+vr&ar*t_+vr<=Vmax()&(xg-GDelta() < ar*(t_^2/2)+vr*t_+xr|xg-GDelta() < ar*(t_^2/2)+vr*t_+xr+(u-1)*ep()*(ar*t_+vr)))`}) ;
assignd(1) ; assignd(1) ;
existsR({`min(ep(),vr/b())/2`}, 1) ; andR(1) ; <(
QE,
andR(1) ; <(
QE,
fullSimplify ; andR(1) ; doall(QE)
)
)
)
)
)
)
)
)
)
)
End.
End.
Lemma "Cross intersection with deadline - Safety".
/*
* Robot must safely cross an intersection.
*
* Robot
* - must cross intersection safely
* - can only drive straight and forward
* - ensures progress towards intersection
*
* Obstacle
* - Drives forward with minimum speed (does not block intersection)
*
* Intersection
* - At position 0 (on both the robot's and the obstacle's path)
*
* Liveness property:
* - Robot can cross intersection
*
* Safety property:
* - Robot always crosses intersection before deadline
* - Robot and obstacle are not at the intersection at the same time
*
*/
Definitions.
R ep(). /* time limit for control decisions */
R b(). /* minimum braking capability of the robot */
R A(). /* maximum acceleration -b <= a <= A */
R Vmin(). /* obstacle minimum speed */
R ixr() = ( 0 ). /* position of intersection on path of robot */
R ixo() = ( 0 ). /* position of intersection on path of obstacle */
R D(). /* Deadline */
R min(R,R).
R max(R,R).
R minV() = ( A()*ep() ).
R stopDist(R v) = ( v^2/(2*b()) ).
R accComp(R v) = ( (A()/b() + 1)*(A()/2*ep()^2 + ep()*v) ).
B OAfterX(R xo) <-> ( xo>ixo() ).
B RAfterX(R xr) <-> ( xr>ixr() ).
B bounds() <-> ( /* Bounds for global constants */
A() > 0 /* Working engine */
& b() > 0 /* Working brakes */
& ep() > 0 /* Controller reaction time */
& Vmin() > 0
& D() >= ep() & RAfterX(xr + A()/2*(D() - ep)^2)
).
B initialState() <-> ( /* Somewhere before intersection initially */
vr = 0
& vo>=Vmin()
& xr < ixr()
& ixr()-xr < A()/2*(D()-ep())^2
& T = min(0, (xo-ixo())/Vmin()) - ep()
).
B assumptions() <-> (bounds() & initialState()). /* Under these assumptions we guarantee safety */
B safetyloopinv() <-> (
0 <= vr & Vmin()<=vo & (RAfterX(xr) | OAfterX(xo) | xr + stopDist(vr) < ixr() |
(vr>0 & ( xo+vo*(ixr()-xr)/vr+A/2*((ixr()-xr)/vr)^2 < ixo()
| ixo() < xo + Vmin()*(ixr()-xr)/vr))
)
).
B deadlineloopinv() <-> (
0 <= vr & Vmin()<=vo
& T <= (xo-ixo())/Vmin()
& ( T <= 0 & RAfterX(xr + A()/2*(D() - ep)^2)
| T > 0 & RAfterX(xr + vr*(max(0,D()-T)) + A()/2*(max(0,D()-T))^2) )
).
HP obstacle ::= { ao := *; ?-b()<=ao&ao<=A(); }.
HP robot ::= {
if (OAfterX(xo)) {
ar := A();
} else { if (RAfterX(xr)) {
ar := *; ?-b()<=ar&ar<=A();
} else { if (/*PassFaster*/ vr>0 & ( xo+vo*(ixr()-xr)/vr+A()/2*((ixr()-xr)/vr)^2 < ixo()
| ixo() < xo + Vmin()*(ixr()-xr)/(vr+A()*ep()) ) ) {
ar := *; ?0<=ar&ar<=A();
} else { if (/*PassCoast*/ vr>0 & ixo() < xo + Vmin()*(ixr()-xr)/vr) {
ar := 0;
} else { /* 1D Model 3 */
ar := -b();
++ ?vr = 0; ar := 0;
++ ?xr + stopDist(vr) + accComp(vr) < ixr(); ar := A();
}}}}
}.
HP dyn ::= { {xr' = vr, vr' = ar, xo'=vo, vo'=ao, t' = 1, T'=1 & t <= ep() & vr >= 0 & vo>=Vmin() } }.
HP dwcxd ::= {
{
obstacle;
{ robot; t := 0; }
dyn;
}*
}.
End.
ProgramVariables.
R xr. /* robot position: x */
R vr. /* robot translational velocity */
R ar. /* robot translational acceleration */
R xo. /* obstacle position */
R vo. /* obstacle velocity */
R ao. /* obstacle acceleration */
R t. /* control cycle time */
R T. /* remaining time until robot must start driving (i.e., until obstacle has passed the intersection) */
End.
Problem.
assumptions() -> [ dwcxd; ]( (xr=ixr() -> xo!=ixo()) & (T>=D() -> RAfterX(xr)) )
End.
Tactic "Proof Lemma: Cross intersection with deadline - Safety".
tactic leafQE as ( print({`Proving arithmetic`}); QE; done );
tactic unfoldQEL as ( (doall(orL('L)))*; doall(leafQE; done); done );
implyR(1) ; boxAnd(1) ; andR(1) ; <(
loop({`0<=vr&Vmin()<=vo&(xr>0|xo>0|xr+vr^2/(2*b()) < 0|vr>0&(xo+vo*(0-xr)/vr+A()/2*((0-xr)/vr)^2 < 0|0 < xo+Vmin()*(0-xr)/vr))`}, 1) ; <(
leafQE,
leafQE,
boxAnd(1) ; andR(1) ; <(
composeb(1) ; composeb(1.1) ; GV(1) ; GV(1.0) ; unfold ; dW(1) ; leafQE,
notAnd(1.0.1.0.0.1.1.1.1.1.1.1.0.0) ; notGreater(1.0.1.0.0.1.1.1.1.1.1.1.0.0.0) ; notLess(1.0.1.0.0.1.1.1.1.1.1.1.0.0.1) ; notAnd(1.0.1.0.0.1.1.1.1.1.0.0) ; notOr(1.0.1.0.0.1.1.1.1.1.0.0.1) ; notLess(1.0.1.0.0.1.1.1.1.1.0.0.1.0) ; notLess(1.0.1.0.0.1.1.1.1.1.0.0.1.1) ; notGreater(1.0.1.0.0.1.1.1.0.0) ; notGreater(1.0.1.0.0.1.1.1.1.1.0.0.0) ;
unfold ; <(
diffInvariant({`xo>=old(xo)`}, 1) ; dW(1) ; leafQE
,
diffInvariant({`xr>=old(xr)`}, 1) ; dW(1) ; leafQE
,
fullSimplify ; hideL('L=={`D()>=ep()`}) ;
diffInvariant({`t>=0&vr=old(vr)+ar*t&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t+ar*t^2/2&xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; andR(1) ; <(
hideL('L=={`xr_0+vr_0^2/(2*b()) < 0|xo_0+vo_0*(-xr_0)/vr_0+A()/2*((-xr_0)/vr_0)^2 < 0|0 < xo_0+Vmin()*(-xr_0)/vr_0`}) ; hideL('L=={`xo_0+vo_0*(-xr_0)/vr_0+A()/2*((-xr_0)/vr_0)^2 < 0|0 < xo_0+Vmin()*(-xr_0)/(vr_0+A()*ep())`}) ; leafQE,
orR('R)*3 ; hideL('L=={`xr_0+vr_0^2/(2*b()) < 0|xo_0+vo_0*(-xr_0)/vr_0+A()/2*((-xr_0)/vr_0)^2 < 0|0 < xo_0+Vmin()*(-xr_0)/vr_0`}) ; andR(4) ; <(
leafQE,
orR('R) ; andL('L)* ; orL(-10) ; <(
edit({`vr_0<=vr&vr<=vr_0+A()*t`}, 'L=={`vr=vr_0+ar*t`}) ; hideL('L=={`t<=ep()`}) ; hideL('L=={`ep()>0`}) ; edit({`xr_0+vr_0*t<=xr&xr<=xr_0+vr_0*t+A()*t^2/2`}, 'L=={`xr=xr_0+vr_0*t+ar*t^2/2`}) ; edit({`xo_0+Vmin()*t<=xo&xo<=xo_0+vo_0*t+A()*t^2/2`}, 'L=={`xo=xo_0+vo_0*t+ao*t^2/2`}) ; edit({`vo<=vo_0+A()*t`}, 'L=={`vo=vo_0+ao*t`}) ; hideL('L=={`-b()<=ao`}) ; hideL('L=={`ao<=A()`}) ; hideL('L=={`0<=ar`}) ; hideL('L=={`ar<=A()`}) ; edit({`vo>0`}, 'L=={`vo>=Vmin()`}) ; edit({`vo_0>0`}, 'L=={`Vmin()<=vo_0`}) ; hideL('L=={`b()>0`}) ; allL2R('L=={`t_0=0`}) ; hideL('L=={`t_0=0`}) ; hideL('L=={`xo_0<=0`}) ; hideL('L=={`xr_0<=0`}) ; hideR('R=={`0 < xo+Vmin()*(-xr)/vr`}) ; hideR('R=={`xr+vr^2/(2*b()) < 0`}) ; hideR('R=={`xo>0`}) ; leafQE,
edit({`0 < xo_0+Vmin()*(-xr_0)/(vr_0+A()*t)`}, 'L=={`0 < xo_0+Vmin()*(-xr_0)/(vr_0+A()*ep())`}) ; hideL('L=={`t<=ep()`}) ; hideL('L=={`ep()>0`}) ; hideR('R=={`xo+vo*(-xr)/vr+A()/2*((-xr)/vr)^2 < 0`}) ; hideR('R=={`xr+vr^2/(2*b()) < 0`}) ; hideL('L=={`-b()<=ao`}) ; hideL('L=={`b()>0`}) ; edit({`vr_0<=vr&vr<=vr_0+A()*t`}, 'L=={`vr=vr_0+ar*t`}) ; edit({`xr_0+vr_0*t<=xr&xr<=xr_0+vr_0*t+A()*t^2/2`}, 'L=={`xr=xr_0+vr_0*t+ar*t^2/2`}) ; edit({`xo_0+Vmin()*t<=xo&xo<=xo_0+vo_0*t+A()*t^2/2`}, 'L=={`xo=xo_0+vo_0*t+ao*t^2/2`}) ; edit({`vo<=vo_0+A()*t`}, 'L=={`vo=vo_0+ao*t`}) ; hideL('L=={`0<=ar`}) ; hideL('L=={`ar<=A()`}) ; hideL('L=={`ao<=A()`}) ; hideL('L=={`xo_0<=0`}) ; hideL('L=={`xr_0<=0`}) ; edit({`0 < vr`}, 'L=={`vr>=0`}) ; leafQE
)
)
)
,
fullSimplify ;
diffInvariant({`t>=0&vr=old(vr)&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t&xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; andR(1) ; <(
leafQE,
orR('R)*3 ; hideR('R=={`xr>0`}) ; hideR('R=={`xo>0`}) ; hideR('R=={`xr+vr^2/(2*b()) < 0`}) ; andR(1) ; <(
leafQE,
orR(1) ; hideR('R=={`xo+vo*(-xr)/vr+A()/2*((-xr)/vr)^2 < 0`}) ; andL(-10) ; hideL('L=={`xo_0+vo_0*(-xr_0)/vr_0+A()/2*((-xr_0)/vr_0)^2>=0`}) ; leafQE
)
)
,
fullSimplify ;
diffInvariant({`t>=0&vr=old(vr)-b()*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t-b()*t^2/2`}, 1) ;
dW(1) ; leafQE
,
hideL('L=={`vr<=0|0>=xo+Vmin()*(0-xr)/vr`}) ;
hideL('L=={`vr<=0|xo+vo*(0-xr)/vr+A()/2*((0-xr)/vr)^2>=0&0>=xo+Vmin()*(0-xr)/(vr+A()*ep())`}) ;
diffInvariant({`vr=old(vr)`}, 1) ;
diffInvariant({`xr=old(xr)`}, 1) ;
fullSimplify ; dW(1) ; leafQE
,
fullSimplify ;
diffInvariant({`t>=0&vr=old(vr)+A()*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t+A()*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; andR(1) ; <(
leafQE,
orR('R)*3 ; hideL('L=={`t_0=0`}) ; hideL('L=={`-b()<=ao`}) ; hideL('L=={`ao<=A()`}) ; hideL('L=={`D()>=ep()`}) ; hideL('L=={`xo_0<=0`}) ; hideR('R=={`vr>0&(xo+vo*(-xr)/vr+A()/2*((-xr)/vr)^2 < 0|0 < xo+Vmin()*(-xr)/vr)`}) ; hideR('R=={`xr>0`}) ; hideR('R=={`xo>0`}) ;
hideL('L=={`xr_0+vr_0^2/(2*b()) < 0|vr_0>0&(xo_0+vo_0*(-xr_0)/vr_0+A()/2*((-xr_0)/vr_0)^2 < 0|0 < xo_0+Vmin()*(-xr_0)/vr_0)`}) ; orL(-7) ; <(
fullSimplify ; leafQE,
orL(-6) ; <(
leafQE,
hideL('L=={`xo_0+vo_0*(-xr_0)/vr_0+A()/2*((-xr_0)/vr_0)^2>=0&0>=xo_0+Vmin()*(-xr_0)/(vr_0+A()*ep())`}) ;
leafQE
)
)
)
)
)
),
loop({`0<=vr&Vmin()<=vo&T<=(xo-0)/Vmin()&(T<=0&xr+A()/2*(D()-ep())^2>0|T>0&xr+vr*max((0,D()-T))+A()/2*max((0,D()-T))^2>0)`}, 1) ; <(
leafQE,
leafQE,
notAnd(1.0.1.0.0.1.1.1.1.1.1.1.0.0) ; notGreater(1.0.1.0.0.1.1.1.1.1.1.1.0.0.0) ; notLess(1.0.1.0.0.1.1.1.1.1.1.1.0.0.1) ; notAnd(1.0.1.0.0.1.1.1.1.1.0.0) ; notOr(1.0.1.0.0.1.1.1.1.1.0.0.1) ; notLess(1.0.1.0.0.1.1.1.1.1.0.0.1.0) ; notLess(1.0.1.0.0.1.1.1.1.1.0.0.1.1) ; notGreater(1.0.1.0.0.1.1.1.0.0) ; notGreater(1.0.1.0.0.1.1.1.1.1.0.0.0) ; boxAnd(1) ; andR(1) ; <(
composeb(1) ; composeb(1.1) ; GV(1) ; GV(1.0) ; unfold ; dW(1) ; leafQE,
boxAnd(1) ; andR(1) ; <(
composeb(1) ; composeb(1.1) ; GV(1) ; GV(1.0) ; unfold ; dW(1) ; leafQE,
boxAnd(1) ; andR(1) ; <(
composeb(1) ; composeb(1.1) ; composeb(1.1) ; GV(1.1) ; unfold ;
diffInvariant({`t>=0&T=old(T)+t&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; leafQE
,
unfold ; <(
diffInvariant({`t>=0&T=old(T)+t&vr=old(vr)+A()*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t+A()*t^2/2`}, 1) ;
dW(1) ; prop ; doall(leafQE)
,
hideL('L=={`!xo>0`}) ;
diffInvariant({`t>=0&T=old(T)+t&vr=old(vr)+ar*t&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t+ar*t^2/2&xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; orR(1) ; edit({`T>0&xr+vr*abbrv(max((0,D()-T)))+A()/2*max((0,D()-T))^2>0`}, 'R=={`T>0&xr+vr*max((0,D()-T))+A()/2*max((0,D()-T))^2>0`}) ;
edit({`abbrv=expand(max((0,D()-T)))`}, 'L=={`abbrv=max((0,D()-T))`}) ;
edit({`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*max((0,D()-T_0))+A()/2*abbrv(max((0,D()-T_0)))^2>0`}, 'L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*max((0,D()-T_0))+A()/2*max((0,D()-T_0))^2>0`}) ;
edit({`abbrv_0=expand(max((0,D()-T_0)))`}, 'L=={`abbrv_0=max((0,D()-T_0))`}) ; andR(1) ; <(
andR(2) ; <(
leafQE,
hideR('R=={`T<=0`}) ; hideL('L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv_0+A()/2*abbrv_0^2>0`}) ;
hideL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; orL(-17) ; <(
leafQE,
leafQE
)
),
orL('L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv_0+A()/2*abbrv_0^2>0`}) ; <(
orL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ; <(
orL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; <(
leafQE,
leafQE
),
hideR(2=={`T>0&xr+vr*abbrv+A()/2*abbrv^2>0`}) ; leafQE
),
hideR(2=={`T>0&xr+vr*abbrv+A()/2*abbrv^2>0`}) ; orL(-18) ; <(
orL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; <(
leafQE,
leafQE
),
orL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; <(
leafQE,
leafQE
)
)
)
),
diffInvariant({`t>=0&T=old(T)+t&vr>=old(vr)&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xr>=old(xr)+old(vr)*t&xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; orR(1) ; hideL('L=={`xo_0+vo_0*(0-xr_0)/vr_0+A()/2*((0-xr_0)/vr_0)^2 < 0|0 < xo_0+Vmin()*(0-xr_0)/(vr_0+A()*ep())`}) ;
edit({`T>0&xr+vr*abbrv(max((0,D()-T)))+A()/2*max((0,D()-T))^2>0`}, 'R=={`T>0&xr+vr*max((0,D()-T))+A()/2*max((0,D()-T))^2>0`}) ;
edit({`abbrv=expand(max((0,D()-T)))`}, 'L=={`abbrv=max((0,D()-T))`}) ;
edit({`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv(max((0,D()-T_0)))+A()/2*max((0,D()-T_0))^2>0`}, 'L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*max((0,D()-T_0))+A()/2*max((0,D()-T_0))^2>0`}) ;
edit({`abbrv_0=expand(max((0,D()-T_0)))`}, 'L=={`abbrv_0=max((0,D()-T_0))`}) ;
andR(1) ; <(
andR(2) ; <(
leafQE,
unfoldQEL
),
andR(2) ; <(
hideL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; hideL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ;
orL('L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv_0+A()/2*abbrv_0^2>0`}) ; <(
leafQE,
leafQE
),
hideR('R=={`xr+A()/2*(D()-ep())^2>0`}) ;
unfoldQEL
)
),
diffInvariant({`t>=0&T=old(T)+t&vr=old(vr)&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t&xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; orR(1) ;
edit({`T>0&xr+vr*abbrv(max((0,D()-T)))+A()/2*max((0,D()-T))^2>0`}, 'R=={`T>0&xr+vr*max((0,D()-T))+A()/2*max((0,D()-T))^2>0`}) ;
edit({`abbrv=expand(max((0,D()-T)))`}, 'L=={`abbrv=max((0,D()-T))`}) ;
edit({`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*max((0,D()-T_0))+A()/2*abbrv(max((0,D()-T_0)))^2>0`}, 'L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*max((0,D()-T_0))+A()/2*max((0,D()-T_0))^2>0`}) ;
edit({`abbrv_0=expand(max((0,D()-T_0)))`}, 'L=={`abbrv_0=max((0,D()-T_0))`}) ; andR(1) ; <(
andR(2) ; <(
leafQE,
hideL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; orL('L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv_0+A()/2*abbrv_0^2>0`}) ; <(
hideL('L=={`vr_0<=0|xo_0+vo_0*(0-xr_0)/vr_0+A()/2*((0-xr_0)/vr_0)^2>=0&0>=xo_0+Vmin()*(0-xr_0)/(vr_0+A()*ep())`}) ;
orL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ; doall(leafQE)
,
orL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ; <(
leafQE,
leafQE
)
)
),
andR(2) ; <(
hideL('L=={`vr_0<=0|xo_0+vo_0*(0-xr_0)/vr_0+A()/2*((0-xr_0)/vr_0)^2>=0&0>=xo_0+Vmin()*(0-xr_0)/(vr_0+A()*ep())`}) ;
hideL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ;
unfoldQEL
,
unfoldQEL
)
),
diffInvariant({`t>=0&T=old(T)+t&vr=old(vr)-b()*t&vo=old(vo)+ao*t`}, 1) ;
diffInvariant({`xr=old(xr)+old(vr)*t-b()*t^2/2&xo=old(xo)+old(vo)*t+ao*t^2/2`}, 1) ;
dW(1) ; implyR(1) ; orR(1) ; hideL('L=={`t_0=0`}) ;
edit({`T>0&xr+vr*abbrv(max((0,D()-T)))+A()/2*max((0,D()-T))^2>0`}, 'R=={`T>0&xr+vr*max((0,D()-T))+A()/2*max((0,D()-T))^2>0`}) ;
edit({`abbrv=expand(max((0,D()-T)))`}, 'L=={`abbrv=max((0,D()-T))`}) ;
edit({`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv(max((0,D()-T_0)))+A()/2*max((0,D()-T_0))^2>0`}, 'L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*max((0,D()-T_0))+A()/2*max((0,D()-T_0))^2>0`}) ;
edit({`abbrv_0=expand(max((0,D()-T_0)))`}, 'L=={`abbrv_0=max((0,D()-T_0))`}) ;
andR(1) ; <(
andR(2) ; <(
leafQE,
hideL('L=={`vr_0<=0|xo_0+vo_0*(0-xr_0)/vr_0+A()/2*((0-xr_0)/vr_0)^2>=0&0>=xo_0+Vmin()*(0-xr_0)/(vr_0+A()*ep())`}) ;
orL('L=={`T_0<=0&xr_0+A()/2*(D()-ep())^2>0|T_0>0&xr_0+vr_0*abbrv_0+A()/2*abbrv_0^2>0`}) ; <(
orL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ; <(
orL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; <(
leafQE,
leafQE
),
orL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; <(
leafQE,
orL('L=={`vr_0<=0|0>=xo_0+Vmin()*(0-xr_0)/vr_0`}) ; <(
leafQE,
andL('L)*; hideL('L=={`-b()<=ao`}) ; hideR(1=={`T<=0`}) ;
hideL('L=={`0>=xo_0+Vmin()*(0-xr_0)/vr_0`}) ; hideL('L=={`xo=xo_0+vo_0*t+ao*t^2/2`}) ;
hideL('L=={`!xo_0>0`});
leafQE
)
)
),
hideR('R=={`T<=0`}) ; orL('L=={`0>=D()-T_0&max_1=0|0 < D()-T_0&max_1=D()-T_0`}) ; <(
orL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ; <(
leafQE,
leafQE
),
orL('L=={`0>=D()-T&max_0=0|0 < D()-T&max_0=D()-T`}) ; <(
leafQE,
leafQE
)