Skip to content

Commit

Permalink
FM19 tutorial folder
Browse files Browse the repository at this point in the history
  • Loading branch information
@smitsch
smitsch committed Sep 19, 2020
1 parent d91603e commit 2229866
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 36 deletions.
70 changes: 45 additions & 25 deletions tutorials/fm-2019/fm-2019-tutorial.kyx
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
ArchiveEntry "1 Bouncing ball"
ArchiveEntry "FM19/1 Bouncing ball"
Description "Acrophobic Bouncing Ball".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -44,7 +44,7 @@ End.

Illustration "https://lfcps.org/info/fig-bouncing-ball-dark-trace.png".
End.
Exercise "2 Exercise: Runaround Robot"
Exercise "FM19/2 Exercise: Runaround Robot"
Description "CurveBot: run a robot round the bend".

ProgramVariables
Expand Down Expand Up @@ -74,8 +74,10 @@ End.

Illustration "https://lfcps.org/info/fig-Dubins-path-robotesque-1.png".
End.
ArchiveEntry "2 Solution: Runaround Robot"
Description "CurveBot: run a robot round the bend (with definitions)".
/* Exported from KeYmaera X v4.7.4 */

ArchiveEntry "FM19/2 Solution: Runaround Robot"
Description "CurveBot: run a robot round the bend".

ProgramVariables
Real x, y; /* robot x/y position */
Expand All @@ -102,7 +104,23 @@ Problem
] !(x=ox & y=oy)
End.

Tactic "CurveBot: Proof"

Tactic "4 Solution: Runaround Robot: Proof"
implyR(1) ; loop("!(x=ox&y=oy)", 1) ; <(
QE,
id,
composeb(1) ; choiceb(1) ; andR(1) ; <(
unfold ; expand "Q" ; ODE(1),
unfold ; <(
expand "Q" ; ODE(1),
expand "Qline" ; ODE(1)
)
)
)
End.


Tactic "4 Solution: Runaround Robot: Manual Proof"
implyR(1) ; loop("!(x=ox&y=oy)", 1) ; <(
QE,
id,
Expand Down Expand Up @@ -131,21 +149,23 @@ Tactic "CurveBot: Proof"
)
End.

Tactic "CurveBot: automatic"
Tactic "4 Solution: Runaround Robot: automatic"
master
End.

Tactic "CurveBot: unfold"
Tactic "4 Solution: Runaround Robot: unfold"
unfold ; loop("!(x=ox&y=oy)", 1) ; <(
QE,
QE,
unfold ; doall(ODE(1))
)
End.


Illustration "https://lfcps.org/info/fig-Dubins-path-robotesque-1.png".

End.
ArchiveEntry "3 Swirl invariant"
ArchiveEntry "FM19/3 Swirl invariant"
Description "LICS'18 hourglass swirl".

ProgramVariables
Expand All @@ -163,7 +183,7 @@ End.
Illustration "https://lfcps.org/info/fig-invariant-swirl-example.png".
End.

ArchiveEntry "3 Swirl invariant circle"
ArchiveEntry "FM19/3 Swirl invariant circle"
Description "LICS'18 circle swirl".

ProgramVariables
Expand All @@ -180,7 +200,7 @@ End.
Illustration "https://lfcps.org/info/fig-invariant-swirl-example.png".
End.

ArchiveEntry "3 Swirl invariant disc"
ArchiveEntry "FM19/3 Swirl invariant disc"
Description "LICS'18 disc swirl".

ProgramVariables
Expand All @@ -196,7 +216,7 @@ master
End.
Illustration "https://lfcps.org/info/fig-invariant-swirl-example.png".
End.
ArchiveEntry "4 Damped oscillator"
ArchiveEntry "FM19/4 Damped oscillator"
Description "Damped oscillators stay in ellipses".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -228,7 +248,7 @@ Illustration "https://lfcps.org/info/fig-damposc-evo2t-region.png".
End.


ArchiveEntry "4 Increasingly damped oscillator"
ArchiveEntry "FM19/4 Increasingly damped oscillator"
Description "Increasingly damped oscillators stay in ellipses".

Definitions
Expand Down Expand Up @@ -262,7 +282,7 @@ End.

Illustration "https://lfcps.org/info/fig-damped-damped-osc-field-region.png".
End.
ArchiveEntry "5 Kepler two body"
ArchiveEntry "FM19/5 Kepler two body"
Description "Two planets in gravitational force field with one planet as origin, mathematically normalized constants".
Citation "Ernst Hairer. Geometric Numerical Integration. TU Munich 2010".

Expand All @@ -285,18 +305,18 @@ Problem
End.

Tactic "Kepler two body: Proof"
/* requires QE("Mathematica") */
useSolver("Mathematica");
implyR(1) ; dI(1)
End.

Tactic "Kepler two body: Proof"
/* requires QE("Mathematica") */
useSolver("Mathematica");
master
End.

Illustration "https://lfcps.org/info/Kepler.png".
End.
ArchiveEntry "6 Coasting Car"
ArchiveEntry "FM19/6 Coasting Car"
Description "Coasting cars can stop".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -338,7 +358,7 @@ Tactic "Coasting Car: Automatic Proof"
End.

End.
ArchiveEntry "7 Exercise: Accelerating Car"
ArchiveEntry "FM19/7 Exercise: Accelerating Car"
Description "Cars need invariants and control constraints to stop before m".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -367,7 +387,7 @@ Problem /* differential dynamic logic formula */
End.

End.
ArchiveEntry "7 Solution: Accelerating Car"
ArchiveEntry "FM19/7 Solution: Accelerating Car"
Description "Cars don't run stop signs".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -427,7 +447,7 @@ Tactic "Safety of time-triggered car: Automatic"
End.

End.
ArchiveEntry "8 01 Exercise: Speed Control Loop Invariant"
ArchiveEntry "FM19/8 01 Exercise: Speed Control Loop Invariant"
Description "Find a Loop Invariant for Braking".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -464,7 +484,7 @@ End.

End.

ArchiveEntry "8 02 Solution: Speed Control Loop Invariant"
ArchiveEntry "FM19/8 02 Solution: Speed Control Loop Invariant"
Description "Find a Loop Invariant for Braking".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -497,7 +517,7 @@ End.

End.

ArchiveEntry "8 03 Exercise: Speed Control Coasting Condition"
ArchiveEntry "FM19/8 03 Exercise: Speed Control Coasting Condition"
Description "Find a Control Condition for Coasting".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -532,7 +552,7 @@ End.

End.

ArchiveEntry "8 04 Solution: Speed Control Coasting Condition"
ArchiveEntry "FM19/8 04 Solution: Speed Control Coasting Condition"
Description "Find a Control Condition for Coasting".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -579,7 +599,7 @@ End.

End.

ArchiveEntry "8 05 Exercise: Accelerating Car"
ArchiveEntry "FM19/8 05 Exercise: Accelerating Car"
Description "Find a Control Condition for Accelerating".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -615,7 +635,7 @@ End.

End.

ArchiveEntry "8 06 Solution: Accelerating Car"
ArchiveEntry "FM19/8 06 Solution: Accelerating Car"
Description "Find a Control Condition for Coasting".

Definitions /* function symbols cannot change their value */
Expand Down Expand Up @@ -651,7 +671,7 @@ End.

End.

ArchiveEntry "8 07 Car Drives Curve"
ArchiveEntry "FM19/8 07 Car Drives Curve"

Description "Car picks steering to not exceed maximum angular speed".

Expand Down
22 changes: 11 additions & 11 deletions tutorials/fm-2019/make.sh
View file
Original file line number Diff line number Diff line change
@@ -1,21 +1,21 @@
#!/bin/sh
[[ -e tmp.kya ]] && rm tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"1 Bouncing ball\"/" < ../../lics/bouncing-ball-if.kyx >> tmp.kya
sed "s/Exercise *\".*\"/Exercise \"2 Exercise: Runaround Robot\"/" < ../../lics/CurveBotExc.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"2 Solution: Runaround Robot\"/" < ../../lics/CurveBotDef.kyx >> tmp.kya
sed "s/ArchiveEntry *\"\(.*\)\"/ArchiveEntry \"3 \1\"/" <../../lfcps-tutorial/swirl.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"FM19\/1 Bouncing ball\"/" < ../../lics/bouncing-ball-if.kyx >> tmp.kya
sed "s/Exercise *\".*\"/Exercise \"FM19\/2 Exercise: Runaround Robot\"/" < ../../lics/CurveBotExc.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"FM19\/2 Solution: Runaround Robot\"/" < ../../lics/CurveBotDef.kyx >> tmp.kya
sed "s/ArchiveEntry *\"\(.*\)\"/ArchiveEntry \"FM19\/3 \1\"/" <../../lfcps-tutorial/swirl.kyx >> tmp.kya
cat > repls <<- EOM
s/ArchiveEntry *"Damp.*"/ArchiveEntry "4 Damped oscillator"/
s/ArchiveEntry *"Increas.*"/ArchiveEntry "4 Increasingly damped oscillator"/
s/ArchiveEntry *"Damp.*"/ArchiveEntry "FM19\/4 Damped oscillator"/
s/ArchiveEntry *"Increas.*"/ArchiveEntry "FM19\/4 Increasingly damped oscillator"/
EOM
sed -f repls < ../../lics/damposc.kyx >> tmp.kya
sed "s/ArchiveEntry *\"\(.*\)\"/ArchiveEntry \"5 \1\"/" <../../lfcps-tutorial/KeplerProblem.kyx >> tmp.kya
sed "s/ArchiveEntry *\"\(.*\)\"/ArchiveEntry \"FM19\/5 \1\"/" <../../lfcps-tutorial/KeplerProblem.kyx >> tmp.kya

sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"6 Coasting Car\"/" < ../../lfcps-tutorial/CoastingCar.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"7 Exercise: Accelerating Car\"/" < ../../lfcps-tutorial/carExc.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"7 Solution: Accelerating Car\"/" < ../../popltutorial/time-safe.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"FM19\/6 Coasting Car\"/" < ../../lfcps-tutorial/CoastingCar.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"FM19\/7 Exercise: Accelerating Car\"/" < ../../lfcps-tutorial/carExc.kyx >> tmp.kya
sed "s/ArchiveEntry *\".*\"/ArchiveEntry \"FM19\/7 Solution: Accelerating Car\"/" < ../../popltutorial/time-safe.kyx >> tmp.kya

sed "s/ArchiveEntry *\"\(.*\)\"/ArchiveEntry \"8 \1\"/" < speedcontrol.kyx >> tmp.kya
sed "s/ArchiveEntry *\"\(.*\)\"/ArchiveEntry \"FM19\/8 \1\"/" < speedcontrol.kyx >> tmp.kya

perl -pe 's/\xEF\xBB\xBF//g' < tmp.kya > fm-2019-tutorial.kyx
rm tmp.kya
Expand Down

0 comments on commit 2229866

Please sign in to comment.