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

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

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?

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/c3e5a888-34f3-4445-af2d-a6de32e8c20cn%40googlegroups.com.