Sara,
it looks like there are some typos in the invariants for module M2
invariant
(q=2 => y<=d132)&
(s=5 => x<=d222)&
(s=8 => x<=d232)
endinvariant
it looks like the s’s be q’s and the x’s be y’s, i.e.
invariant
(q=2 => y<=d132)&
(q=5 => y<=d222)&
(q=8 => y<=d232)
endinvariant
thanks
Gethin
> On 18 May 2017, at 14:43, Sara Himmiche <sarah...@gmail.com> wrote:
>
> Hi,
> I'm trying to use PRISM with PTA to model a scheduling problem so I have a bunch of modules that are synchronized by event and I put guards on some of them in relation with states of other modules ( model in attachement ). When I do model checking with digital clocks and these property : E [F " all operations are executed".
> Prism find a Timelock that i can't see in the model.
>
> I hope to find help here.
>
> Thanks in advance.
>
>
>
>
> --
> You received this message because you are subscribed to the Google Groups "PRISM model checker" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to prismmodelchecker+unsubscribe@googlegroups.com.
> To post to this group, send email to prismmodelchecker@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.
> <Scheduling.nm>
--
You received this message because you are subscribed to a topic in the Google Groups "PRISM model checker" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/prismmodelchecker/0ZU_Gjft95k/unsubscribe.
To unsubscribe from this group and all its topics, send an email to prismmodelchecker+unsubscribe@googlegroups.com.
To post to this group, send an email to prismmodelchecker@googlegroups.com.