Commit d70efc13 authored by Nicolas Basset's avatar Nicolas Basset
Browse files

Update example/driving_NFM_v2.prism

parent 52f9ee7a
Pipeline #1500 failed with stage
in 18 seconds
pta
module m
s : [0..3] init 0;
x : clock;
y : clock;
invariant
(y<15)
endinvariant
//Coasting to see, save fuel
[a] (s=0) & (y>2) & (y<15) -> (s'=3) & (x'=0) & (y'=0); //acceleration to coasting 00
[b] (s=3) & (y>1) & (y<15) -> (s'=2) & (x'=0) & (y'=0); //coasting to brake 01
[c] (s=3) & (y>1) & (y<15) -> (s'=0) & (x'=0) & (y'=0); //coasting to acceleration 10
//Braking cycle
[d] (s=0) & (y>2) & (y<15) -> (s'=2) & (x'=0) & (y'=0); //acceleration to braking 01
[e] (s=1) & (y>1) & (y<2) & (x<10) -> (s'=2) & (y'=0); //coasting to brake 01
[f] (s=2) & (y>1) & (y<2) & (x<10) -> (s'=1) & (y'=0); //brake to coasting 00
[g] (s=2) & (y>1) & (x>3) & (x<10) -> (s'=0) & (x'=0) & (y'=0); //brake to acceleration 10
[h] (s=1) & (y>1) & (x>3) & (x<10) -> (s'=0) & (x'=0) & (y'=0); //coasting to acceleration 10
endmodule
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment