# [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 writer in the community of Writer will eventually be writing

EXTENDS FiniteSets

VARIABLES Resource
vars == Resource

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

FreeActors == Actors \ BusyActors

/\ 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} ]

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

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?

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.