Hulp
Deze pagina aan uw boek toevoegen
Boek weergeven (27 pagina's)
Pagina's suggererenCruisecontrol
Inhoud
- 1 Inleiding
- 2 Focus
- 3 Structuur
- 4 Onderdeelspecificaties
- 5 De specificatie van het geheel
- 6 De correctheidsstelling
- 7 Het bewijs
- 8 Bewijs Scenario
Inleiding
De inleiding en conclusie schrijf je als laatste, niet eer je weet wat in te leiden is.
Focus
Het bestudeerde fragment van de realiteit
We hebben gekozen voor het artefact Cruisecontrol+, ook wel Adaptive Cruise Control genaamd. Het betreft een embedded system in auto's en bevat (naast de benodigde elektronica en software) een controlemechanisme, vaak in de vorm van een soort hendel, waarmee je de Cruise Control kan instellen. Dit controlemechanisme is door middel van een draad met het cruisecontrolsysteem verbonden. Daarnaast is de auto aan de voorzijde uitgerust met (infrarood)sensoren, die tevens door middel van een kabel verbonden zijn met het cruisecontrolsysteem. Ook ontvangt het systeem (via een andere kabel) een digitaal signaal van de snelheidsmeter, wat een (nauwkeurige) representatie van de huidige snelheid van de auto geeft. Tevens geeft het rempedaal een elektrisch signaal aan het systeem wanneer deze ingedrukt wordt. Datzelfde geldt voor het koppelingspedaal. Tot slot is het cruisecontrolsysteem via een kabel verbonden met de boordcomputer van de auto.
Het gezichtspunt
We onderzoeken de werking van de Adaptive Cruise Control.
Specificatie in natuurlijke taal
Voor alle tijdstippen geldt, als voor alle tijdstippen in het interval tussen het tijdstip dat de snelheid gepind is en het huidige tijdstip geldt dat de Cruise Control is aangesloten op een 12V-spanningsbron, als er gedurende de tijdstippen dat de snelheid gepind is en het huidige tijdstip niet nog een keer een snelheid gepind is en niet op de koppeling of rem is getrapt dan geldt dat
als er aan de twee secondenregel wordt voldaan, dan is er een snelheid gepind en is er niet nog een keer een snelheid gepind tussen dat moment en het huidige tijdstip en dan wordt, als er niet maximaal gas wordt gegeven en de ingestelde snelheid groter is dan de huidige snelheid, het gaspercentage verhoogd met 1 en de rem Ratio op 0 gezet.
en
als er aan de tweesecondenregel wordt voldaan of niet aan de tweesecondenregel en er is geen sprake van een gevaarlijke afstand tot de voorganger, dan is er een moment waarop de snelheid is gepind en is de snelheid niet nog een keer is gepind tussen dat moment en het huidige tijdstip en als het gaspercentage nog groter of gelijk is aan 1 wordt dit verminderd met 1 en als het gaspercentage al kleiner dan 1 is en het rempercentage nog kleiner dan 99 dan wordt het gaspercentage op 0 gezet en verhogen we het rempercentage met 1.
en
als de huidige snelheid overeenkomt met de gepinde snelheid dan blijft het gas- en rempercentage gelijk aan wat het was.
Externe Fenomenen
- De invoerspanning van 12 volt;
- De snelheid van de auto;
- De afstand tot de voorganger;
- De status van het rem- en koppelingspedaal (of deze ingedrukt zijn of niet);
- De status van het controlemechanisme, waarmee de cruise control kan worden ingesteld c.q. aangepast: signalen voor het vastzetten, verhogen en verlagen van de snelheid;
- De huidige gas- en remratio: de ratio (als in: het percentage) waarop de motor c.q. remmen momenteel werken ten opzichte van hun maximale capaciteit.
Interne Fenomenen
- Signaal dat aangeeft of de Cruisecontrol aan staat; tevens spanningsvoorziening;
- Signaal dat afgegeven wordt vanuit het Bedieningspaneel om die invoer van de gebruiker door te geven (dit is een verzameling van mogelijke signalen);
- Ingestelde snelheid: signaal dat aangeeft of op een gegeven moment de ingestelde snelheid gelijk is aan een gegeven snelheid;
- Interne snelheid: signaal dat aangeeft of op een gegeven moment de werkelijke snelheid gelijk is aan een gegeven snelheid.
Waarom?
We hebben voor dit onderwerp gekozen omdat technologie in auto's steeds meer de standaard wordt. Deze techniek bestaat weliswaar al enige tijd, maar naarmate het verder doorontwikkeld wordt neemt het steeds meer taken van de bestuurder over. Dat kan praktisch en veilig zijn, maar wanneer het niet aan haar specificatie voldoet juist erg gevaarlijk. Daarom hebben wij dit onderwerp gekozen. Achteraf willen we onszelf de vraag kunnen stellen: hadden er ongelukken kunnen gebeuren wanneer wij het door ons ontworpen systeem eerst geïmplementeerd hadden, en toen pas de correctheid van de specificatie hadden bewezen?
Qua domeinkennis is vooral kennis over de werking van cruise control (en wat common sense kennis van auto's) nodig. Deze is in zekere mate aanwezig in het groepje doordat we allemaal al eens auto hebben gereden. Daarnaast zijn er op het internet veel betrouwbare bronnen over te raadplegen. Wij verwachten dus geen problemen wat betreft domeinkennis.
Wat wordt formeel behandeld?
Alle eigenschappen die reeds in de Specificatie in natuurlijke taal hierboven beschreven staan, vinden wij dusdanig belangrijk dat we ze zeker in de correctheidsstelling op willen nemen.
Vereenvoudigingen
We negeren de tijd die het in de praktijk kost om elektrische signalen door te geven. Ook gaan we ervan uit dat berekeningen direct resultaat opleveren; er is geen rekentijd. Wel rekenen we een constante tijdsduur van 100 ms (0,1 seconde) voor de tijd tussen het moment waarop het systeem aan de boordcomputer meldt dat er versnelt moet worden, en het moment waarop de motor daadwerkelijk extra vermogen genereert.
Het signaal van de Control naar de CPU en de Snelheidsmeter dat aangeeft dat de Cruisecontrol aan staat, zorgt tevens voor de benodigde spanning voor de CPU en Snelheidsmeter.
Structuur
Functioneel netwerk
De ImageMap-extensie is niet geïnstalleerd.
Onderdelen
| Naam | Korte informele specificatie |
|---|---|
| Bedieningspaneel | Kijkt welke knoppen/pedalen door de gebruiker zijn ingedrukt. |
| Control | Bepaalt, afhankelijk van enkele invoersignalen (sommigen lopen via het Bedieningspaneel), of de CPU en Snelheidsmeter aan moeten en voorziet deze van spanning. |
| CPU | Dient als rekencentrum van het systeem; bepaalt wat de nieuwe gas- en remratio worden. |
| Snelheidsmeter | Verwerkt de huidige snelheid van de auto tot een intern signaal en onthoudt de ingestelde snelheid. |
Het domeinmodel
| Domeinen | Omschrijving |
|---|---|
| S | De afstand in meters uitgedrukt in reële getallen |
| V | De snelheid in km/h uitgedrukt in reële getallen |
| T | De tijd in deciseconden (1/10 seconde) uitgedrukt in reële getallen |
| P | Percentages in reële getallen groter of gelijk aan 0 en kleiner of gelijk aan 100 |
| KS | Verzameling van knopsignalen die het bedieningspaneel van de Cruise Control kan afgeven |
| Predikaat | Type | Betekenis | Meting |
|---|---|---|---|
| spanningIn t | T → B | De Cruise Control is aangesloten op een 12V-spanningsbron. | Meten of er spanning op de spanningsingang van de Cruise Control staat met een voltmeter |
| pinSnelheid t | T → B | Op tijdstip t is de snelheid gepind. | Kijken of de pinknop is ingedrukt op tijdstip t |
| koppelingIn t | T → B | De koppeling is ingetrapt op tijdstip t | Kijken of de koppeling is ingetrapt op tijdstip t |
| remIn t | T → B | De rem is ingetrapt op tijdstip t | Kijken of de rem is ingetrapt op tijdstip t |
| CCaan t | T → B | De CPU moet de auto op de ingestelde snelheid houden of de minimale volgafstand aanhouden | Meten of er spanning staat op de kabel met een voltmeter |
| huidigeSnelheid v t | V → T → B | De snelheid v, die de auto op tijdstip t heeft. | Kijk op moment t op de snelheidsmeter van de auto |
| afstandVoorganger s t | S → T → B | De afstand s waarop de auto, waarin de Cruise Control zit, zich bevindt op tijdstip t. | Met behulp van een infraroodsensor de afstand tot de voorganger meten |
| gasRatio p t | P → T → B | Het percentage gas p (hoe ver het gaspedaal is ingedrukt) op tijdstip t. | Meten hoe ver de gasklep in de carburateur van de motor geopend is |
| remRatio p t | P → T → B | Het percentage rem p (hoe ver het rempedal is ingedrukt) op stijdstip t. | Meten hoe ver de zuigerstang in de hoofdremcilinder is gedrukt |
| verhoogSnelheid t | T → B | Op tijdstip t is op de knop snelheid verhogen gedrukt. | Kijken of op tijdstip t de knop om de snelheid te verhogen is ingedrukt |
| verlaagSnelheid t | T → B | Op tijdstip t is op de knop snelheid verlagen gedrukt. | Kijken of op tijdstip t de knop om de snelheid te verlagen is ingedrukt |
| signaalAfgegeven k t | KS → T → B | Op tijdstip t wordt er een knopsignaal k afgegeven. | Meten met een voltmeter op de datakabel van het bedieningspaneel. |
| ingesteldeSnelheid v t | V → T → B | Op tijdstip t is de ingestelde snelheid gelijk aan v. | Met een portsniffer de datakabel bekijken welke snelheid op het moment is ingesteld |
| interneSnelheid v t | V → T → B | Op tijdstip t is de huidige snelheid gelijk is aan v |
| Functie | Type | Betekenis |
|---|---|---|
| opgeslagenSnelheid t | T → V | De opgeslagen snelheid v op tijdstip t |
| afstandPerSeconde v | V → S | Geeft aan hoe groot de afstand is die de auto per seconde aflegt bij snelheid v in meters. |
Hulpdefinities
tweeSecondenRegel
Kijkt of er wordt voldaan aan de tweesecondenregel: de afstand tot de voorganger is gelijk of groter dan de afstand die de auto met zijn huidige snelheid in twee secondes gaat afleggen.
Definition tweeSecondenRegel (v:V)(s:S) := ( (afstandPerSeconde v) * 2) < s .
Voor specificatie van het geheel
heeftSpanning
Kijkt of er sinds het moment dat de gebruiker de snelheid heeft vastgelegd tot het huidige moment spanning staat op de cruise control.
Definition heeftSpanning (t:T) := exists t1:T, pinSnelheid t1 /\ t1 <= t /\ ( forall t2:T, t2 in [t1,t] -> spanningIn t2 ) .
isIngeschakeld
Kijkt of de CruiseControl op moment t ingeschakeld is.
Definition isIngeschakeld (t:T) :=
exists t1:T,
t1 <= t
/\
pinSnelheid t1
/\
~(exists t2:T,
t2 in (t1, t]
/\
pinSnelheid t2
)
/\
~(exists t2:T,
t2 in [t1, t]
/\
koppelingIn t2
/\
remIn t2
)
.
snelheidTeVerhogen
Kijkt of dat de snelheid verhoogt kan worden; kijkt eerst wat de huidige snelheid van de auto is, wat zijn afstand tot de voorganger is. Vervolgens kijkt hij of er aan de twee seconde-regel wordt voldaan. Als dat goed gaat en er niet al maximaal gas wordt gegeven en de huidige snelheid lager is dan de ingestelde snelheid, gaan we de snelheid verhogen (door de rem "los" te laten, dus het ratio op 0 te zetten) en het gas toe te laten nemen.
Definition snelheidTeVerhogen (t:T) :=
forall v:V,
forall s:S,
huidigeSnelheid v t /\ afstandVoorganger s t
->
tweeSecondenRegel v s
->
(exists t1:T,
pinSnelheid t1
/\
~(exists t2:T,
t2 in (t1, t]
/\
pinSnelheid t2
)
/\
(forall ingesteld:V,
huidigeSnelheid ingesteld t1
->
(forall g:P,
gasRatio g t /\ g <= 99
->
ingesteld > v
->
gasRatio (g+1) (t+1) /\ remRatio 0 (t+1)
)
)
)
.
gevaarlijkeAfstand
Kijkt of dat er dringend gevaar is: dat we te dichtbij de voorganger rijden. Eerst zoeken we de huidige gas- en remratio, huidige afstand tot de voorganger en de afstand tot de voorganger en slaan die waardes op in de variabelen. Als we met de huidige snelheid in één seconde de voorganger dreigen te passeren en er wordt nog niet maximaal geremd, dan zetten we gelijk het gas op 0 en laten we de remratio met 1% toenemen.
Definition gevaarlijkeAfstand (t:T):=
forall v:V,
forall s:S,
forall g:P,
forall r:P,
gasRatio g t
/\
remRatio r t
/\
huidigeSnelheid v t
/\
afstandVoorganger s t
->
r <= 99
->
s - (afstandPerSeconde v) <= 0 /\ gasRatio 0 (t+1) /\ remRatio (r+1) (t+1)
.
snelheidTeVerlagen
Kijkt of dat de snelheid verlaagd moet worden; kijkt eerst wat de huidige snelheid van de auto is, wat zijn afstand tot de voorganger is en wat de huidige gas- en remratio zijn. Deze waardes slaat hij op de in de desbetreffende variabelen en kijkt of dan niet de twee seconden regel wordt geschonden en of we niet te dicht op de voorganger zitten. Als dat allemaal klopt dan laten we het gas afnemen tot 0 en wordt de remratio 0. Als het gas al kleiner dan 1 is en er wordt nog niet maximaal geremd, betekent dat we extra moeten gaan remmen. Dus verhogen we de remratio met 1%.
Definition snelheidTeVerlagen (t:T):=
forall v:V,
forall s:S,
huidigeSnelheid v t /\ afstandVoorganger s t
->
tweeSecondenRegel v s
\/
~gevaarlijkeAfstand t /\ ~tweeSecondenRegel v s
->
(exists t1:T,
pinSnelheid t1
/\
~(exists t2:T,
t2 in (t1, t]
/\
pinSnelheid t2
)
/\
(forall ingesteld:V,
huidigeSnelheid ingesteld t1
->
(forall g:P, forall r:P,
gasRatio g t /\ remRatio r t
->
v > ingesteld
->
( g >= 1
->
gasRatio (g-1) (t+1) /\ remRatio 0 (t+1)
)
/\
( ~ g >= 1 /\ r <= 99
->
gasRatio 0 (t+1) /\ remRatio (r+1) (t+1)
)
)
)
.
goedeSnelheidEnAfstand
Als er uiteindelijk helemaal niets van bovenstaande definities worden gebruikt, betekent dat er niets aan de hand is, dus dat we met de huidige rem-/gaswaardes kunnen verder rijden. Dus deze laten we dan ook ongewijzigd.
Definition goedeSnelheidEnAfstand (t:T) :=
forall v:V,
forall g:P,
forall r:P,
huidigeSnelheid v t
/\
gasRatio g t
/\
remRatio r t
->
(forall ingesteld:V,
ingesteldeSnelheid ingesteld t
->
v = ingesteld
->
gasRatio g (t+1)
/\
remRatio r (t+1)
)
.
Voor CPU
snelheidPlusCPU
De snelheid op het moment is lager dan de ingestelde snelheid en er wordt voldaan aan de twee seconden-regel. De snelheid mag dus worden verhoogd, als het gasratio niet hoger is dan 99 en het remratio wordt op 0 gezet.
Definition snelheidPlusCPU (t:T)(v:V):=
forall g:P,
forall s:S,
forall v2:V,
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
v < v2
/\
tweeSecondenRegel v s
->
g<=99
->
gasRatio (g+1) (t+1)
/\
remRatio 0 (t+1)
.
snelheidMinCPU
Als de huidige snelheid hoger is dan de ingestelde snelheid, maar de twee seconden-regel wordt niet gebroken, dan wordt er gas afgenomen (als deze al niet op 0% staat).
Definition snelheidMinCPU (t:T)(v:V) :=
forall g:P,
forall s:S,
forall v2:V,
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
v > v2
/\
tweeSecondenRegel v s
->
g>=1
->
gasRatio (g-1) (t+1)
/\
remRatio 0 (t+1)
.
snelheidGevaarlijkHoogCPU
Als de huidige snelheid hoger is dan de ingestelde snelheid en de afstand tot de voorganger is te klein geworden, dan gaan we het gasratio op 0% zetten en laten we het remratio toenemen.
forall g:P,
forall s:S,
forall v2:V,
forall r:P,
~tweeSecondenRegel v s
/\
remRatio r t
/\
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
s<afstandPerSeconde v /\ r<=99
->
gasRatio 0 (t+1) /\ remRatio (r+1) (t+1)
.
snelheidNietGevaarlijkHoogCPU
Als de huidige snelheid hoger is dan de ingestelde snelheid en de afstand tot de voorganger is niet te klein geworden, dan gaan we eerst het gasratio verlagen tot 0% en vervolgens gaan we het remratio steeds verhogen.
forall g:P,
forall s:S,
forall v2:V,
forall r:P,
~tweeSecondenRegel v s
/\
remRatio r t
/\
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
s>=afstandPerSeconde v
->
(
(
g>=1
->
gasRatio (g-1) (t+1) /\ remRatio 0 (t+1)
)
/\
(
g<1 /\ r<=99
->
remRatio (r+1) (t+1) /\ gasRatio 0 (t+1)
)
)
.
goedeSnelheidCPU
Als de ingestelde snelheid gelijk is aan de huidige snelheid en er wordt voldaan aan de 2secondenregel, dan blijft op tijdstip t+100 het gasratio gelijk en staat het remratio op 0.
Definition goedeSnelheidCPU (t:T)(v:V):=
forall g:P,
forall s:S,
forall v2:V,
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
v = v2
/\
tweeSecondenRegel v s
->
gasRatio g (t+1)
/\
remRatio 0 (t+1)
.
Onderdeelspecificaties
Bedieningspaneel
Definition Bedieningspaneel:= forall t:T, ( signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t ) /\ ( signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t ) /\ ( signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t ) /\ ( signaalAfgegeven koppelingInSign t <-> koppelingIn t ) /\ ( signaalAfgegeven remInSign t <-> remIn t ) .
Omschrijving
Voor alle tijdstippen geldt:
- dat er een signaal wordt afgegeven om de snelheid te pinnen op een bepaald tijdstip dan en slechts dan als er op dat tijdstip op de knop is gedrukt om de snelheid te pinnen;
- en dat er een signaal wordt afgegeven om de snelheid te verhogen op een bepaald tijdstip dan en slechts dan als er op dat tijdstip op de knop is gedrukt om de snelheid te verhogen;
- en dat er een signaal wordt afgegeven om de snelheid te verlagen op een bepaald tijdstip dan en slechts dan als er op dat tijdstip op de knop is gedrukt om de snelheid te verlagen;
- en dat er een signaal wordt afgegeven dat de koppeling is ingedrukt op een bepaald tijdstip dan en slechts dan als er op dat tijdstip op de koppeling is ingedrukt;
- en dat er een signaal wordt afgegeven dat de rem is ingedrukt op een bepaald tijdstip dan en slechts dan als er op dat tijdstip op de rem is ingedrukt.
Verantwoording
-
Control
Definition Control := forall t:T, heeftSpanning t -> ( exists t1:T, t1 <= t /\ signaalAfgegeven pinSnelheidSign t1 /\ ( forall t2:T, t2 in [t1, t] -> ~signaalAfgegeven koppelingInSign t2 /\ ~signaalAfgegeven remInSign t2 ) ) -> CCaan t .
Omschrijving
Voor alle tijdstippen geldt dat als er spanning staat op de Control gedurende de gehele sessie, dan geldt dat als er een tijdstip bestaat kleiner of gelijk aan het gekozen tijdstip waarop geldt dat er geen signaal is afgegeven dat de rem is ingedrukt en dat er geen signaal is afgegeven dat de koppeling is ingedrukt, dan geldt dat de Cruise Control aan staat.
Verantwoording
-
CPU
Definition CPU := forall t:T, forall v:V, CCaan t /\ interneSnelheid v t -> snelheidPlusCPU t v /\ snelheidMinCPU t v /\ snelheidGevaarlijkHoogCPU t v /\ snelheidNietGevaarlijkHoogCPU t v /\ goedeSnelheidCPU t v .
Snelheidsmeter
Definition Snelheidsmeter :=
(forall t:T,
( signaalAfgegeven pinSnelheidSign t
->
(forall v:V,
huidigeSnelheid v t
->
opgeslagenSnelheid t = v
/\
(forall t1:T,
( exists t2:T,
~CCaan t2
/\
t1 in [t, t2)
/\
CCaan t1
)
->
(
( signaalAfgegeven verhoogSnelheidSign t1
->
opgeslagenSnelheid (t1) = (v+1)
)
/\
( ~ signaalAfgegeven verhoogSnelheidSign t1
->
(
( signaalAfgegeven verlaagSnelheidSign t1
->
opgeslagenSnelheid (t1) = (v-1)
)
/\
(
~ signaalAfgegeven verlaagSnelheidSign t1
->
opgeslagenSnelheid (t1) = v
)
)
)
)
)
)
)
/\
ingesteldeSnelheid (opgeslagenSnelheid t) t
)
/\
(
forall v:V,
forall t:T,
interneSnelheid v t
<->
huidigeSnelheid v t
)
.
Omschrijving
Op een moment t geldt dat de snelheid is gepind en op alle momenten tussen t en het moment waarop de cruise control uit staat moet gelden dat: als het verhoogsnelheid signaal is gegeven dat de opgeslagen snelheid vanaf dat moment hoger, idem voor lager. Als zowel de snelheid niet is verhoogd en niet is verlaagd dan wordt de huidige snelheid opgeslagen. Bovendien vertaalt hij de interne snelheid naar de huidige snelheid en vice versa.
Verantwoording
De specificatie van het geheel
Wij hebben er in overleg met David Jansen voor gekozen om in plaats van de gehele definitie van de CruiseControl alleen de essentiële delen in de specificatie van het geheel te stoppen. Dit hebben wij gedaan in verband met de complexiteit van de formalisaties. Hiervoor in de plaats bewijzen wij ook een scenario dat wel deze complexe gevallen dekt.
Definition AdaptiveCruiseControl :=
forall t:T,
heeftSpanning t
->
isIngeschakeld t
->
snelheidTeVerhogen t
/\
snelheidTeVerlagen t
/\
goedeSnelheidEnAfstand t
.
De specificatie van het scenario
Definition Scenario :=
forall t : T,
pinSnelheid t
/\
verhoogSnelheid (t+100)
/\
verlaagSnelheid (t+150)
/\
gasRatio 50 t
/\
(forall v:V, forall s:S,
tweeSecondenRegel v s
)
/\
(forall t1:T,
t1 in [t, t+201]
->
afstandVoorganger 200 t1
/\
(
verhoogSnelheid t1
->
t1 = t+100
)
/\
(
verlaagSnelheid t1
->
t1 = t+150
)
/\
spanningIn t1
/\
~koppelingIn t1
/\
~remIn t1
)
/\
(forall t2:T,
t2 in [t, t+100]
->
huidigeSnelheid 80 t2
)
->
(forall g:P,
( gasRatio g t
->
gasRatio (g+1) (t+101)
)
/\
( gasRatio g (t+150)
->
gasRatio (g-1) (t+151)
)
)
.
De correctheidsstelling
Theorem Correctheidsstelling : Control -> CPU -> Snelheidsmeter -> Bedieningspaneel -> AdaptiveCruiseControl.
Theorem ScenarioStelling : Control -> CPU -> Snelheidsmeter -> Bedieningspaneel -> Scenario.
Het bewijs
<source lang="coq"> Require Import BenB. Set Undo 1000.
(* Domeinmodel: *) Definition S := R. Definition V := R. Definition T := R. Definition P := R. Inductive KS : Set := pinSnelheidSign | verhoogSnelheidSign | verlaagSnelheidSign | koppelingInSign | remInSign.
(* Predikaten *) Variable spanningIn : T -> B. Variable pinSnelheid : T -> B. Variable koppelingIn : T -> B. Variable remIn : T -> B. Variable CCaan : T -> B. Variable huidigeSnelheid : V -> T -> B. Variable afstandVoorganger : S -> T -> B. Variable gasRatio : P -> T -> B. Variable remRatio : P -> T -> B. Variable verhoogSnelheid : T -> B. Variable verlaagSnelheid : T -> B. Variable signaalAfgegeven : KS -> T -> B. Variable ingesteldeSnelheid : V -> T -> B. Variable interneSnelheid : V -> T -> B.
(* Functies *) Variable opgeslagenSnelheid : T -> V. Variable afstandPerSeconde : V -> S.
(* Hulpdefinities *)
Definition tweeSecondenRegel (v:V)(s:S) :=
( (afstandPerSeconde v) * 2) < s
.
(* Hulpdefinities voor specificatie van het geheel *)
Definition heeftSpanning (t:T) :=
exists t1:T,
pinSnelheid t1 /\ t1 <= t
/\
(
forall t2:T,
t2 in [t1,t]
->
spanningIn t2
)
.
Definition isIngeschakeld (t:T) := exists t1:T,
t1 <= t
/\
pinSnelheid t1
/\
~(exists t2:T,
t2 in (t1, t]
/\
pinSnelheid t2
)
/\
~(exists t2:T,
t2 in [t1, t]
/\
koppelingIn t2
/\
remIn t2
)
.
Definition snelheidTeVerhogen (t:T) := forall v:V,
forall s:S,
huidigeSnelheid v t /\ afstandVoorganger s t
->
tweeSecondenRegel v s
->
(exists t1:T,
pinSnelheid t1
/\
~(exists t2:T,
t2 in (t1, t]
/\
pinSnelheid t2
)
/\
(forall ingesteld:V,
huidigeSnelheid ingesteld t1
->
(forall g:P,
gasRatio g t /\ g <= 99
-> ingesteld > v -> gasRatio (g+1) (t+1) /\ remRatio 0 (t+1)
)
)
)
.
Definition gevaarlijkeAfstand (t:T):=
forall v:V,
forall s:S,
forall g:P,
forall r:P,
gasRatio g t
/\
remRatio r t
/\
huidigeSnelheid v t
/\
afstandVoorganger s t
->
r <= 99
->
s - (afstandPerSeconde v) <= 0 /\ gasRatio 0 (t+1) /\ remRatio (r+1) (t+1)
.
Definition snelheidTeVerlagen (t:T):=
forall v:V,
forall s:S,
huidigeSnelheid v t /\ afstandVoorganger s t
->
tweeSecondenRegel v s
\/
~gevaarlijkeAfstand t /\ ~tweeSecondenRegel v s
->
(exists t1:T,
pinSnelheid t1
/\
~(exists t2:T,
t2 in (t1, t]
/\
pinSnelheid t2
)
/\
(forall ingesteld:V,
huidigeSnelheid ingesteld t1
->
(forall g:P, forall r:P,
gasRatio g t /\ remRatio r t
->
v > ingesteld
->
( g >= 1 -> gasRatio (g-1) (t+1) /\ remRatio 0 (t+1) ) /\ ( ~ g >= 1 /\ r <= 99 -> gasRatio 0 (t+1) /\ remRatio (r+1) (t+1) )
)
)
)
.
Definition goedeSnelheidEnAfstand (t:T) := forall v:V,
forall g:P,
forall r:P,
huidigeSnelheid v t /\
gasRatio g t
/\
remRatio r t
->
(forall ingesteld:V, ingesteldeSnelheid ingesteld t -> v = ingesteld -> gasRatio g (t+1) /\ remRatio r (t+1) ) .
(* Hulpdefinities voor de CPU *)
Definition snelheidPlusCPU (t:T)(v:V):= forall g:P,
forall s:S,
forall v2:V,
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
v < v2
/\
tweeSecondenRegel v s
->
g<=99
->
gasRatio (g+1) (t+1)
/\
remRatio 0 (t+1)
.
Definition snelheidMinCPU (t:T)(v:V) := forall g:P,
forall s:S,
forall v2:V,
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
v > v2
/\
tweeSecondenRegel v s
->
g>=1
->
gasRatio (g-1) (t+1)
/\
remRatio 0 (t+1)
.
Definition snelheidGevaarlijkHoogCPU (t:T)(v:V) := forall g:P,
forall s:S,
forall v2:V,
forall r:P,
~tweeSecondenRegel v s
/\
remRatio r t
/\
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
s<afstandPerSeconde v /\ r<=99
->
gasRatio 0 (t+1) /\ remRatio (r+1) (t+1)
.
Definition snelheidNietGevaarlijkHoogCPU (t:T)(v:V) := forall g:P,
forall s:S,
forall v2:V,
forall r:P,
~tweeSecondenRegel v s
/\
remRatio r t
/\
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
s>=afstandPerSeconde v
->
(
(
g>=1
->
gasRatio (g-1) (t+1) /\ remRatio 0 (t+1)
)
/\
(
g<1 /\ r<=99
->
remRatio (r+1) (t+1) /\ gasRatio 0 (t+1)
)
)
.
Definition goedeSnelheidCPU (t:T)(v:V):=
forall g:P,
forall s:S,
forall v2:V,
gasRatio g t
/\
afstandVoorganger s t
/\
ingesteldeSnelheid v2 t
->
v = v2
/\
tweeSecondenRegel v s
->
gasRatio g (t+1)
/\
remRatio 0 (t+1)
.
(* Onderdelen *)
Definition Bedieningspaneel:=
forall t:T,
( signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t )
/\
( signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t )
/\
( signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t )
/\
( signaalAfgegeven koppelingInSign t <-> koppelingIn t )
/\
( signaalAfgegeven remInSign t <-> remIn t )
.
Definition Control :=
forall t:T,
heeftSpanning t
->
( exists t1:T,
t1 <= t
/\
signaalAfgegeven pinSnelheidSign t1
/\
( forall t2:T,
t2 in [t1, t]
->
~signaalAfgegeven koppelingInSign t2
/\
~signaalAfgegeven remInSign t2
)
)
->
CCaan t
.
Definition CPU :=
forall t:T,
forall v:V,
CCaan t
/\
interneSnelheid v t
->
snelheidPlusCPU t v
/\
snelheidMinCPU t v
/\
snelheidGevaarlijkHoogCPU t v
/\
snelheidNietGevaarlijkHoogCPU t v
/\
goedeSnelheidCPU t v
.
Definition Snelheidsmeter :=
(forall t:T,
( signaalAfgegeven pinSnelheidSign t -> (forall v:V, huidigeSnelheid v t -> opgeslagenSnelheid t = v /\ (forall t1:T, ( exists t2:T, ~CCaan t2 /\ t1 in [t, t2) /\ CCaan t1 ) -> ( ( signaalAfgegeven verhoogSnelheidSign t1 -> opgeslagenSnelheid (t1) = (v+1) ) /\ ( ~ signaalAfgegeven verhoogSnelheidSign t1 -> ( ( signaalAfgegeven verlaagSnelheidSign t1 -> opgeslagenSnelheid (t1) = (v-1) ) /\ ( ~ signaalAfgegeven verlaagSnelheidSign t1 -> opgeslagenSnelheid (t1) = v ) ) ) ) ) ) ) /\ ingesteldeSnelheid (opgeslagenSnelheid t) t
)
/\
(
forall v:V,
forall t:T,
interneSnelheid v t
<->
huidigeSnelheid v t
)
.
(* Specificatie van het geheel *)
Definition AdaptiveCruiseControl :=
forall t:T,
heeftSpanning t
->
isIngeschakeld t
->
snelheidTeVerhogen t
/\
snelheidTeVerlagen t
/\
goedeSnelheidEnAfstand t
.
(* Specificatie van het scenario *)
Definition Scenario :=
forall t : T,
pinSnelheid t
/\
verhoogSnelheid (t+100)
/\
verlaagSnelheid (t+150)
/\
gasRatio 50 t
/\
(forall v:V, forall s:S, tweeSecondenRegel v s ) /\
(forall t1:T,
t1 in [t, t+201]
->
afstandVoorganger 200 t1 /\
(
verhoogSnelheid t1
->
t1 = t+100
)
/\
(
verlaagSnelheid t1
->
t1 = t+150
)
/\
spanningIn t1
/\
~koppelingIn t1
/\
~remIn t1
)
/\
(forall t2:T,
t2 in [t, t+100]
->
huidigeSnelheid 80 t2
)
->
(forall g:P,
( gasRatio g t
->
gasRatio (g+1) (t+101)
)
/\
( gasRatio g (t+150)
->
gasRatio (g-1) (t+151)
)
)
.
(* Lemma's en Axiom's *)
Axiom gasGelijk : forall tbegin:T, forall teind:T, tbegin < teind -> (forall vbegin:V, (forall tussen:T, tussen in [tbegin, teind] -> huidigeSnelheid vbegin tussen /\ (forall sbegin:S, tweeSecondenRegel vbegin sbegin ) ) -> (forall g:P, gasRatio g tbegin /\ gasRatio g teind /\ huidigeSnelheid vbegin tbegin ) ) .
(* Correctheidsstelling *)
Theorem Correctheidsstelling : Control -> CPU -> Snelheidsmeter -> Bedieningspaneel -> AdaptiveCruiseControl.
(* Bewijs *) imp_i s1. imp_i s2. imp_i s3. imp_i s4. unfold AdaptiveCruiseControl. all_i tijd1. imp_i s5. imp_i s6. con_i.
Focus 2. con_i. Focus 2. unfold goedeSnelheidEnAfstand. all_i snelheidr. all_i gasr. all_i remr. imp_i s9. all_i ingesteldr. imp_i s10. imp_i s11. con_i. unfold CPU in s2. unfold goedeSnelheidCPU in s2. con_e1 (remRatio 0 (tijd1 +1)). imp_e (1=1 /\ tweeSecondenRegel 1 2). imp_e (gasRatio gasr tijd1 /\ afstandVoorganger 2 tijd1 /\ ingesteldeSnelheid 1 tijd1). all_e (forall v2:V, gasRatio gasr tijd1 /\
afstandVoorganger 2 tijd1 /\ ingesteldeSnelheid v2 tijd1 -> 1 = v2 /\ tweeSecondenRegel 1 2 -> gasRatio gasr (tijd1 + 1) /\ remRatio 0 (tijd1 + 1) ) 1.
all_e (forall s:S, forall v2:V, gasRatio gasr tijd1 /\
afstandVoorganger s tijd1 /\ ingesteldeSnelheid v2 tijd1 -> 1 = v2 /\ tweeSecondenRegel 1 s -> gasRatio gasr (tijd1 + 1) /\ remRatio 0 (tijd1 + 1) ) 2.
all_e (forall g:P, forall s : S, forall v2 : V,
gasRatio g tijd1 /\ afstandVoorganger s tijd1 /\ ingesteldeSnelheid v2 tijd1 -> 1 = v2 /\ tweeSecondenRegel 1 s -> gasRatio g (tijd1 + 1) /\ remRatio 0 (tijd1 + 1) ) gasr.
con_e2 (snelheidNietGevaarlijkHoogCPU tijd1 1). con_e2 (snelheidGevaarlijkHoogCPU tijd1 1). con_e2 (snelheidMinCPU tijd1 1). con_e2 (snelheidPlusCPU tijd1 1). imp_e (CCaan tijd1 /\ interneSnelheid 1 tijd1).
all_e (forall v:V, CCaan tijd1 /\ interneSnelheid v tijd1 ->
snelheidPlusCPU tijd1 v /\ snelheidMinCPU tijd1 v /\ snelheidGevaarlijkHoogCPU tijd1 v /\ snelheidNietGevaarlijkHoogCPU tijd1 v /\ (forall (g : P) (s : S) (v2 : V), gasRatio g tijd1 /\ afstandVoorganger s tijd1 /\ ingesteldeSnelheid v2 tijd1 -> v = v2 /\ tweeSecondenRegel v s -> gasRatio g (tijd1 + 1) /\ remRatio 0 (tijd1 + 1)) ) 1.
all_e (forall t:T,
forall v : V, CCaan t/\ interneSnelheid v t-> snelheidPlusCPU t v /\ snelheidMinCPU t v /\ snelheidGevaarlijkHoogCPU t v /\ snelheidNietGevaarlijkHoogCPU t v /\ (forall (g : P) (s : S) (v2 : V), gasRatio g t/\ afstandVoorganger s t/\ ingesteldeSnelheid v2 t -> v = v2 /\ tweeSecondenRegel v s -> gasRatio g (t + 1) /\ remRatio 0 (t + 1))) tijd1.
assumption. con_i. unfold Control in s1. imp_e ( (exists t1 : T,
t1 <= tijd1 /\
signaalAfgegeven pinSnelheidSign t1 /\
(forall t2 : T,
t2 in [t1, tijd1] ->
~ signaalAfgegeven koppelingInSign t2 /\
~ signaalAfgegeven remInSign t2))).
imp_e (heeftSpanning tijd1).
all_e (forall t : T,
heeftSpanning t ->
(exists t1 : T,
t1 <= t /\
signaalAfgegeven pinSnelheidSign t1 /\
(forall t2 : T,
t2 in [t1, t] ->
~ signaalAfgegeven koppelingInSign t2 /\
~ signaalAfgegeven remInSign t2)) -> CCaan t ) tijd1.
assumption. assumption. unfold isIngeschakeld in s6. exi_e (exists t1 : T,
t1 <= tijd1 /\
pinSnelheid t1 /\
~ (exists t2 : T, t2 in (t1, tijd1] /\ pinSnelheid t2) /\
~ (exists t2 : T, t2 in [t1, tijd1] /\ koppelingIn t2 /\ remIn t2)) pintijd s12.
assumption.
exi_i pintijd. con_i. con_e1 (pinSnelheid pintijd /\
~ (exists t2 : T, t2 in (pintijd, tijd1] /\ pinSnelheid t2) /\
~
(exists t2 : T, t2 in [pintijd, tijd1] /\ koppelingIn t2 /\ remIn t2)).
assumption. con_i.
unfold Bedieningspaneel in s4.
iff_e2 (pinSnelheid pintijd). con_e1 ( (signaalAfgegeven verhoogSnelheidSign pintijd <-> verhoogSnelheid pintijd) /\
(signaalAfgegeven verlaagSnelheidSign pintijd <-> verlaagSnelheid pintijd ) /\
(signaalAfgegeven koppelingInSign pintijd <-> koppelingIn pintijd ) /\
(signaalAfgegeven remInSign pintijd <-> remIn pintijd )).
all_e (forall t : T,
(signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t) /\
(signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t) /\
(signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t) /\
(signaalAfgegeven koppelingInSign t <-> koppelingIn t) /\
(signaalAfgegeven remInSign t <-> remIn t) ) pintijd.
assumption. con_e1 (~ (exists t2 : T, t2 in (pintijd, tijd1] /\ pinSnelheid t2) /\
~(exists t2 : T, t2 in [pintijd, tijd1] /\ koppelingIn t2 /\ remIn t2)).
con_e2 (pintijd<=tijd1). assumption.
(* Correctheidsstelling scenario *) Theorem ScenarioStelling : Control -> CPU -> Snelheidsmeter -> Bedieningspaneel -> Scenario.
(* Bewijs *) imp_i control. imp_i cpu. imp_i snelheid. imp_i bp.
unfold Scenario. all_i x. imp_i scen. all_i g1. con_i. imp_i a2. unfold CPU in cpu. unfold snelheidPlusCPU in cpu. con_e1 (remRatio 0 (x+101)). imp_e (g1 <= 99). imp_e (80 < 81 /\ tweeSecondenRegel 80 200). imp_e (gasRatio g1 (x+100) /\ afstandVoorganger 200 (x+100) /\ ingesteldeSnelheid 81 (x+100)). all_e (forall v2:V, gasRatio g1 (x+100) /\ afstandVoorganger 200 (x+100) /\ ingesteldeSnelheid v2 (x+100) ->
80 < v2 /\ tweeSecondenRegel 80 200 ->
g1 <= 99 -> gasRatio (g1 + 1) (x + 101) /\ remRatio 0 (x+101)) 81.
all_e (forall s:S, forall v2:V, gasRatio g1 (x+100) /\ afstandVoorganger s (x+100) /\ ingesteldeSnelheid v2 (x+100) ->
80 < v2 /\ tweeSecondenRegel 80 s ->
g1 <= 99 -> gasRatio (g1 + 1) (x + 101) /\ remRatio 0 (x+101)) 200.
all_e (forall g:P, forall s:S, forall v2:V, gasRatio g (x+100) /\ afstandVoorganger s (x+100) /\ ingesteldeSnelheid v2 (x+100) ->
80 < v2 /\ tweeSecondenRegel 80 s ->
g <= 99 -> gasRatio (g + 1) (x + 101) /\ remRatio 0 (x+101)) g1.
con_e1 (snelheidMinCPU (x+100) 80 /\ snelheidGevaarlijkHoogCPU (x+100) 80 /\ snelheidNietGevaarlijkHoogCPU (x+100) 80 /\ goedeSnelheidCPU (x+100) 80). imp_e (CCaan (x+100) /\ interneSnelheid 80 (x+100)). all_e (forall v:V, CCaan (x + 100) /\ interneSnelheid v (x + 100) ->
(forall (g : P) (s : S) (v2 : V), gasRatio g (x + 100) /\ afstandVoorganger s (x + 100) /\ ingesteldeSnelheid v2 (x + 100) -> v < v2 /\ tweeSecondenRegel v s -> g <= 99 -> gasRatio (g + 1) (x + 101) /\ remRatio 0 (x + 101)) /\ snelheidMinCPU (x + 100) v /\ snelheidGevaarlijkHoogCPU (x + 100) v /\ snelheidNietGevaarlijkHoogCPU (x + 100) v /\ goedeSnelheidCPU (x + 100) v) 80.
replace (x+101) with (x+100+1). all_e (forall t:T,forall v : V,
CCaan t /\ interneSnelheid v t -> (forall (g : P) (s : S) (v2 : V), gasRatio g t /\ afstandVoorganger s t /\ ingesteldeSnelheid v2 t -> v < v2 /\ tweeSecondenRegel v s -> g <= 99 -> gasRatio (g + 1) (t + 1) /\ remRatio 0 (t + 1)) /\ snelheidMinCPU t v /\ snelheidGevaarlijkHoogCPU t v /\ snelheidNietGevaarlijkHoogCPU t v /\ goedeSnelheidCPU t v ) (x+100).
hyp cpu. lin_solve.
fold CPU in cpu. unfold Control in control. con_i. imp_e ((exists t1 : T,
t1 <= (x+100) /\
signaalAfgegeven pinSnelheidSign t1 /\
(forall t2 : T,
t2 in [t1, (x+100)] ->
~ signaalAfgegeven koppelingInSign t2 /\
~ signaalAfgegeven remInSign t2))).
imp_e (heeftSpanning (x+100)). all_e (forall t : T, heeftSpanning t ->
(exists t1 : T,
t1 <= t /\
signaalAfgegeven pinSnelheidSign t1 /\
(forall t2 : T,
t2 in [t1, t] ->
~ signaalAfgegeven koppelingInSign t2 /\
~ signaalAfgegeven remInSign t2)) -> CCaan t) (x+100).
hyp control.
fold Control in control. unfold heeftSpanning. exi_i x. con_i. con_e1 (verhoogSnelheid (x + 100) /\
verlaagSnelheid (x + 150) /\
gasRatio 50 x /\
(forall (v : V) (s : S), tweeSecondenRegel v s) /\
(forall t1 : T,
t1 in [x, x + 201] ->
afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) /\
(forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2)).
hyp scen.
con_i. lin_solve.
all_i c. imp_i intv. con_e1 (~koppelingIn c /\ ~remIn c). con_e2 ( verlaagSnelheid c -> c = x + 150 ). con_e2 ( verhoogSnelheid c -> c = x + 100). con_e2 (afstandVoorganger 200 c). imp_e (c in [x, x+201]). all_e ( forall t1:T, t1 in [x, x + 201] ->
afstandVoorganger 200 t1 /\ (verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\ spanningIn t1 /\ ~koppelingIn t1 /\ ~remIn t1) c.
con_e1 ( forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2 ). con_e2 (forall (v : V) (s : S), tweeSecondenRegel v s). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
interval. con_i. con_e1 ( c <= x+100 ). hyp intv.
imp_e ( c<= x+100 ). imp_i truc. lin_solve.
con_e2 ( x<=c ). hyp intv. exi_i x. con_i. lin_solve.
con_i. unfold Bedieningspaneel in bp. iff_e2 (pinSnelheid x). con_e1 ((signaalAfgegeven verhoogSnelheidSign x <-> verhoogSnelheid x) /\
(signaalAfgegeven verlaagSnelheidSign x <-> verlaagSnelheid x) /\
(signaalAfgegeven koppelingInSign x <-> koppelingIn x) /\
(signaalAfgegeven remInSign x <-> remIn x)).
all_e (forall t:T, (signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t) /\
(signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t) /\
(signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t) /\
(signaalAfgegeven koppelingInSign t <-> koppelingIn t) /\
(signaalAfgegeven remInSign t <-> remIn t)) x.
hyp bp.
con_e1 (verhoogSnelheid (x + 100) /\
verlaagSnelheid (x + 150) /\
gasRatio 50 x /\
(forall (v : V) (s : S), tweeSecondenRegel v s) /\
(forall t1 : T,
t1 in [x, x + 201] -> afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) /\
(forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2)).
hyp scen.
all_i y. imp_i a3. con_i. neg_i (koppelingIn y) a4. con_e1 (~remIn y). con_e2 (spanningIn y). con_e2 (verlaagSnelheid y -> y = x + 150). con_e2 (verhoogSnelheid y -> y = x + 100). con_e2 (afstandVoorganger 200 y). imp_e (y in [x, x + 201]). all_e (forall t1:T, t1 in [x, x + 201] -> afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\ (verlaagSnelheid t1 -> t1 = x + 150) /\ spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) y.
con_e1 (forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2). con_e2 ((forall (v : V) (s : S), tweeSecondenRegel v s)). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
interval. con_i. con_e1 (y <= x + 100). hyp a3. imp_e (y <= x + 100). imp_i truc. lin_solve. con_e2 (x <= y). hyp a3.
unfold Bedieningspaneel in bp. iff_e1 (signaalAfgegeven koppelingInSign y). con_e1 (signaalAfgegeven remInSign y <-> remIn y). con_e2 (signaalAfgegeven verlaagSnelheidSign y <-> verlaagSnelheid y). con_e2 (signaalAfgegeven verhoogSnelheidSign y <-> verhoogSnelheid y). con_e2 (signaalAfgegeven pinSnelheidSign y <-> pinSnelheid y). all_e (forall t:T, (signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t) /\
(signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t) /\ (signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t) /\ (signaalAfgegeven koppelingInSign t <-> koppelingIn t) /\ (signaalAfgegeven remInSign t <-> remIn t)) y.
hyp bp. hyp a4.
unfold Bedieningspaneel in bp. neg_i (remIn y) a5. con_e2 (~koppelingIn y). con_e2 (spanningIn y). con_e2 (verlaagSnelheid y -> y = x + 150). con_e2 (verhoogSnelheid y -> y = x + 100). con_e2 (afstandVoorganger 200 y). imp_e (y in [x, x + 201]). all_e (forall t1:T, t1 in [x, x + 201] -> afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\ (verlaagSnelheid t1 -> t1 = x + 150) /\ spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) y.
con_e1 (forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2). con_e2 ((forall (v : V) (s : S), tweeSecondenRegel v s)). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
interval. con_i. con_e1 (y <= x+100). hyp a3.
imp_e (y <= x + 100). imp_i a6. lin_solve. con_e2 ( x <= y). hyp a3.
iff_e1 (signaalAfgegeven remInSign y). con_e2 (signaalAfgegeven koppelingInSign y <-> koppelingIn y). con_e2 (signaalAfgegeven verlaagSnelheidSign y <-> verlaagSnelheid y). con_e2 (signaalAfgegeven verhoogSnelheidSign y <-> verhoogSnelheid y). con_e2 (signaalAfgegeven pinSnelheidSign y <-> pinSnelheid y). all_e (forall t:T, (signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t) /\
(signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t) /\ (signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t) /\ (signaalAfgegeven koppelingInSign t <-> koppelingIn t) /\ (signaalAfgegeven remInSign t <-> remIn t)) y.
hyp bp. hyp a5.
unfold Snelheidsmeter in snelheid. iff_e2 (huidigeSnelheid 80 (x + 100)). all_e (forall t:T, interneSnelheid 80 t <-> huidigeSnelheid 80 t) (x + 100). all_e (forall v:V, forall t:T, interneSnelheid v t <-> huidigeSnelheid v t) 80. con_e2 ((forall t : T,
(signaalAfgegeven pinSnelheidSign t ->
forall v : V,
huidigeSnelheid v t ->
opgeslagenSnelheid t = v /\
(forall t1 : T,
(exists t2 : T, ~ CCaan t2 /\ t1 in [t, t2) /\ CCaan t1) ->
(signaalAfgegeven verhoogSnelheidSign t1 ->
opgeslagenSnelheid t1 = v + 1) /\
(~ signaalAfgegeven verhoogSnelheidSign t1 ->
(signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v)))) /\
ingesteldeSnelheid (opgeslagenSnelheid t) t)).
hyp snelheid.
fold Snelheidsmeter in snelheid. fold Control in control. imp_e ((x+100) in [x, x+100]). all_e (forall t2:T, t2 in [x, x+100] -> huidigeSnelheid 80 t2) (x+100). con_e2 ((forall t1 : T,
t1 in [x, x + 201] -> afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1)).
con_e2 ((forall (v : V) (s : S), tweeSecondenRegel v s)). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
interval. con_i. lin_solve. lin_solve.
con_i. con_e1 (huidigeSnelheid 80 x). con_e2 (gasRatio g1 x). apply gasGelijk. lin_solve. all_i tussent. imp_i gasGelijk1. con_i. imp_e (tussent in [x, x+100]). all_e (forall t2:T, t2 in [x, x+100] -> huidigeSnelheid 80 t2) tussent. con_e2 ((forall t1 : T,
t1 in [x, x + 201] -> afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1)).
con_e2 ((forall (v : V) (s : S), tweeSecondenRegel v s)). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen. hyp gasGelijk1.
all_i sb. all_e (forall s:S, tweeSecondenRegel 80 s) sb. all_e (forall v:V, forall s:S, tweeSecondenRegel v s) 80. con_e1 ((forall t1 : T,
t1 in [x, x + 201] -> afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) /\
(forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2)).
con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
con_i. con_e1 ((verhoogSnelheid (x+100) -> (x+100) = x + 100) /\
(verlaagSnelheid (x+100) -> (x+100) = x + 150) /\
spanningIn (x+100) /\ ~ koppelingIn (x+100) /\ ~ remIn (x+100)).
imp_e ( (x+100) in [x, x + 201] ). all_e (forall t1 : T,
t1 in [x, x + 201] ->
afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) (x+100).
con_e1 ((forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2)). con_e2 ((forall (v : V) (s : S), tweeSecondenRegel v s)). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
interval. con_i. lin_solve. lin_solve.
unfold Snelheidsmeter in snelheid. replace 81 with (opgeslagenSnelheid (x+100)). con_e2 ((signaalAfgegeven pinSnelheidSign (x+100) ->
forall v : V,
huidigeSnelheid v (x+100) ->
opgeslagenSnelheid (x+100) = v /\
(forall t1 : T,
(exists t2 : T, ~ CCaan t2 /\ t1 in [(x+100), t2) /\ CCaan t1) ->
(signaalAfgegeven verhoogSnelheidSign t1 ->
opgeslagenSnelheid t1 = v + 1) /\
(~ signaalAfgegeven verhoogSnelheidSign t1 ->
(signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v))))).
all_e ((forall t : T,
(signaalAfgegeven pinSnelheidSign t ->
forall v : V,
huidigeSnelheid v t ->
opgeslagenSnelheid t = v /\
(forall t1 : T,
(exists t2 : T, ~ CCaan t2 /\ t1 in [t, t2) /\ CCaan t1) ->
(signaalAfgegeven verhoogSnelheidSign t1 ->
opgeslagenSnelheid t1 = v + 1) /\
(~ signaalAfgegeven verhoogSnelheidSign t1 ->
(signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v)))) /\
ingesteldeSnelheid (opgeslagenSnelheid t) t)) (x+100).
con_e1 ((forall (v : V) (t : T),
interneSnelheid v t <-> huidigeSnelheid v t)).
hyp snelheid.
replace 81 with (80+1). imp_e (signaalAfgegeven verhoogSnelheidSign (x+100)). con_e1 (~ signaalAfgegeven verhoogSnelheidSign (x+100) ->
(signaalAfgegeven verlaagSnelheidSign (x+100) ->
opgeslagenSnelheid (x+100) = 80 - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign (x+100) ->
opgeslagenSnelheid (x+100) = 80)).
imp_e (exists t2 : T, ~ CCaan t2 /\ (x+100) in [x, t2) /\ CCaan (x+100)). all_e (forall t1 : T,
(exists t2 : T, ~ CCaan t2 /\ t1 in [x, t2) /\ CCaan t1) ->
(signaalAfgegeven verhoogSnelheidSign t1 ->
opgeslagenSnelheid t1 = 80 + 1) /\
(~ signaalAfgegeven verhoogSnelheidSign t1 ->
(signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = 80 - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = 80))) (x+100).
con_e2 (opgeslagenSnelheid x = 80). imp_e (huidigeSnelheid 80 x). all_e (forall v : V,
huidigeSnelheid v x ->
opgeslagenSnelheid x = v /\
(forall t1 : T,
(exists t2 : T, ~ CCaan t2 /\ t1 in [x, t2) /\ CCaan t1) ->
(signaalAfgegeven verhoogSnelheidSign t1 ->
opgeslagenSnelheid t1 = v + 1) /\
(~ signaalAfgegeven verhoogSnelheidSign t1 ->
(signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v)))) 80.
imp_e (signaalAfgegeven pinSnelheidSign x). con_e1 (ingesteldeSnelheid (opgeslagenSnelheid x) x). all_e ((forall t : T,
(signaalAfgegeven pinSnelheidSign t ->
forall v : V,
huidigeSnelheid v t ->
opgeslagenSnelheid t = v /\
(forall t1 : T,
(exists t2 : T, ~ CCaan t2 /\ t1 in [t, t2) /\ CCaan t1) ->
(signaalAfgegeven verhoogSnelheidSign t1 ->
opgeslagenSnelheid t1 = v + 1) /\
(~ signaalAfgegeven verhoogSnelheidSign t1 ->
(signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v - 1) /\
(~ signaalAfgegeven verlaagSnelheidSign t1 ->
opgeslagenSnelheid t1 = v)))) /\
ingesteldeSnelheid (opgeslagenSnelheid t) t)) x.
con_e1 ((forall (v : V) (t : T),
interneSnelheid v t <-> huidigeSnelheid v t)).
hyp snelheid.
fold Snelheidsmeter in snelheid. unfold Bedieningspaneel in bp. iff_e2 (pinSnelheid x). con_e1 ((signaalAfgegeven verhoogSnelheidSign x <-> verhoogSnelheid x) /\
(signaalAfgegeven verlaagSnelheidSign x <-> verlaagSnelheid x) /\
(signaalAfgegeven koppelingInSign x <-> koppelingIn x) /\
(signaalAfgegeven remInSign x <-> remIn x)).
all_e (forall t : T,
(signaalAfgegeven pinSnelheidSign t <-> pinSnelheid t) /\
(signaalAfgegeven verhoogSnelheidSign t <-> verhoogSnelheid t) /\
(signaalAfgegeven verlaagSnelheidSign t <-> verlaagSnelheid t) /\
(signaalAfgegeven koppelingInSign t <-> koppelingIn t) /\
(signaalAfgegeven remInSign t <-> remIn t)) x.
hyp bp. fold Bedieningspaneel in bp. con_e1 (verhoogSnelheid (x + 100) /\
verlaagSnelheid (x + 150) /\
gasRatio 50 x /\
(forall (v : V) (s : S), tweeSecondenRegel v s) /\
(forall t1 : T,
t1 in [x, x + 201] ->
afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1) /\
(forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2)).
hyp scen.
fold Snelheidsmeter in snelheid. imp_e (x in [x, x + 100]). all_e (forall t2 : T, t2 in [x, x + 100] -> huidigeSnelheid 80 t2) x. con_e2 ( (forall t1 : T,
t1 in [x, x + 201] ->
afstandVoorganger 200 t1 /\
(verhoogSnelheid t1 -> t1 = x + 100) /\
(verlaagSnelheid t1 -> t1 = x + 150) /\
spanningIn t1 /\ ~ koppelingIn t1 /\ ~ remIn t1)).
con_e2 ((forall (v : V) (s : S), tweeSecondenRegel v s)). con_e2 (gasRatio 50 x). con_e2 (verlaagSnelheid (x + 150)). con_e2 (verhoogSnelheid (x + 100)). con_e2 (pinSnelheid x). hyp scen.
interval. con_i. lin_solve. lin_solve.
fold Snelheidsmeter in snelheid. </source>
Bewijs Scenario
Download onderstaande bijlage (.doc of .pdf) om het bewijs van het scenario te openen. Dit bewijs liet de SQL-database van de werkplaats crashen wanneer we het hier rechtstreeks neer zouden zetten. De extensie .txt is hier niet toegestaan, dus we hebben hem als zowel .doc als .pdf opgeslagen.
DOC: Bewijs_scenario.doc MIME-type niet toegestaan...
PDF: Bewijs_scenario.pdf Open de PDF met de volledige Adobe Reader, anders gaat het kopiëren niet goed!
