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