diff --git a/prism-examples/firewire/impl/expected.pctl b/prism-examples/firewire/impl/expected.pctl new file mode 100644 index 00000000..cc8914c8 --- /dev/null +++ b/prism-examples/firewire/impl/expected.pctl @@ -0,0 +1,4 @@ +// maximum expected time +R{"time"}max=?[F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ] +// maximum expected rounds +R{"time_sending"}max=?[F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ]