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

Re: [tlaplus]



Hello,

you need to describe the interaction protocol as a state machine, recording the states of policy proposals and describing the possible actions of partners.

Requirements 1 and 2 will be reflected in the protocol: introduce a counter for how many times a proposal has been modified and disallow a "modification" action concerning an adopted proposal.

Requirements 3 and 5 are quantitative. Again, you'll need to introduce appropriate counters. Assuming that nothing is required to happen on any given day, you will not be able to guarantee that any policy has been adopted after 20 days, and assuming that a policy can be adopted immediately after it has been proposed, there is no obvious upper bound on the number of policies (or lower bound on the number of days required) either. By specifying fairness properties and/or minimum delays you may be able to get meaningful results for these questions.

Stephan


On 6 Feb 2019, at 11:19, John Paul Kasse <johnpa...@xxxxxxxxx> wrote:

Hi TLA+ wonderful people
I need help please.
I am using TLA+ to model and check interaction between  6 Partners who are in a business partnership. Partners interact for 20 days to propose and discuss policies to guide their business. Each partner can propose an idea that is either accepted without modification, modified and adopted or rejected by the partners. Once adopted all partners assent to the policy which is then recorded. Each member has equal rights to propose, modify or reject. Once adopted by majority partners the policy is adopted even when some others had rejected it. 
Can i be helped to develop an algorithm or specification expressing this interactivity please and check some properties like;
1. A policy can only be modified 2 times before adoption
2. Modifications sent after adoption are not considered
3. Number of policies that are agreed upon by the end of 20 days
5. What are the minimum days required to attain at least 10 policies

--
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+u...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.