Timelock on PRISM

[Sara Himmiche]

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. 

[Gethin Norman]

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

> --
> 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 prismmodelchec...@googlegroups.com.
> To post to this group, send email to prismmod...@googlegroups.com.
> Visit this group at https://groups.google.com/group/prismmodelchecker.
> For more options, visit https://groups.google.com/d/optout.
> <Scheduling.nm>

[Sara Himmiche]

Hi Gethin, 

Thanks for the quick response indeed it was a modelling mistake. 

2017-05-18 16:02 GMT+02:00 Gethin Norman <gethin...@gmail.com>:

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.