BinyuHuang-nju commented on pull request #1690:
URL: https://github.com/apache/zookeeper/pull/1690#issuecomment-831296902
@Vanlightly @fpj I am very glad to see your replies!!
I have found faults in my spec that resulted in invariant violations about
LocalPrimaryOrder and Integrity.
In writing LocalPrimaryOrder, I wrongly wrote 'A=>B' as 'A /\ B'.
Invariant Integirty means, if some follower delivers one transaction, then
some primary must have broadcast it. But I only considered broadcast in msg
with type PROPOSE from phase3(normal case), and ignored broadcast in msg with
type NEWLEADER from phase2(Sync).
Now, I have fixed these bugs, and have added this commit. You could download
new spec and run models. Until now, by using Servers {s1,s2} and Values
{v1,v2}(it is not important to change CONSTANT Value) as sets of model values,
and adding all invariants that I defined, I have not found errors.
I will run this model and update data tomorrow. Since it is half past ten in
China, I have to go home, and I will check your replies tomorrow.
Thanks again for your attention!! (By the way, since this is a project
independent of zookeeper, and I am a rookie in using Travis CI, how can I pass
Travis CI building?
--
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.
For queries about this service, please contact Infrastructure at:
us...@infra.apache.org
