[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Reader Writer Problem specs : Liveness & TLC



2 - Maybe, because Spec is machine closed?

On Tuesday, February 23, 2021 at 10:58:53 AM UTC+1 Younes wrote:
Hello,

1 - I've written the specs below for the Reader-Writer Problem, and I'm wondering if the Liveness conditions I have set are right. I considered that the liveness conditions are :
  • Every reader in the community of Readers will eventually be reading
  • Every writer in the community of Writer will eventually be writing
-------------------------- MODULE Readers_Writers --------------------------
\*  https://en.wikipedia.org/wiki/Readers%E2%80%93writers_problem

EXTENDS FiniteSets

CONSTANTS Readers, Writers

VARIABLES Resource
vars == Resource

Init == Resource = [ Readers |-> {}, Writers |-> {} ]

Actors == Readers \union Writers
BusyActors == Resource.Readers \union Resource.Writers
FreeActors == Actors \ BusyActors

Reading(actor) == /\ actor \in Readers
                  /\ actor \notin BusyActors
                  /\ Cardinality(Resource.Writers) = 0
                  /\ Resource' = [Resource EXCEPT !.Readers = @ \union {actor} ]
                  
Writing(actor) == /\ actor \in Writers
                  /\ actor \notin BusyActors
                  /\ Cardinality(BusyActors) = 0
                  /\ Resource' = [Resource EXCEPT !.Writers = @ \union {actor }]

StopActivity(actor) == /\ actor \in BusyActors
                       /\ \/ actor \in Resource.Readers /\ Resource' = [Resource EXCEPT !.Readers = @ \ {actor} ]
                          \/ actor \in Resource.Writers /\ Resource' = [Resource EXCEPT !.Writers = @ \ {actor} ]

ReaderShouldBeReading == \A reader \in Readers : [] <> (reader \in Resource.Readers)
WriterShouldBeWriting == \A writer \in Writers : [] <> (writer \in Resource.Writers)

Liveness == ReaderShouldBeReading /\ WriterShouldBeWriting

Next == \E actor \in Actors : Reading(actor) \/ Writing(actor) \/ StopActivity(actor)

Spec == Init /\ [][Next]_vars /\ Liveness

=============================================================================

2 - I have also realized that whether I include the Liveness conditions or not in my Spec, the results, after the model checking, are the same. Why?

results_mc.PNG

3 - Why does the action StopActivity has 0 distinct state? Does that mean TLC doesn't explore it at all? Why is that?

I will also gladly take any comments about the specs for improvement.

Thank you!

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fe531577-cd95-482e-9149-cc49da93aa93n%40googlegroups.com.