tables.zip

[Peter Furniss <peter.furniss@choreology.com>]

  BTPers,

The enclosed zip contains the current version of the state table html and
the "proofs" of the transitions. Slightly modified from the version I put on
the screen at the end of yesterday - it now really is the state table, so
the entries as you see them show the new state the endpoint role goes to
when the event occurs. If it is a hypertext link, it will take you to an
example trace which includes that transition. If the entry  is just in red,
then the simulation runs haven't produced an example (at least since I last
cleared the history files which was after making the last appreciable
change. (Adding the ability to send RESIGN/no-rsp-req *before* receiving
PREPARE, I think (states b1, c1)). I've run about 3 million trials since
then.  Eventually the unseen events will occur, or we can conclude they
can't happen and take them out - I've seen events require 5 million trials
or so to turn up.

The exerciser program keeps the "best" example of each transition, with best
defined as shortest. Sometimes this means it's a rather degenerate case
(e.g. disruption occurs immediately afterwards), but it avoids getting the
cases where the same message is sent repeatedly. (the next-event choosing
bit of the exerciser isn't terribly bright)

The state tables shown are as they are currently, having applied the
decisions in San Jose, including:
	hazard (problem) can be detected and possibly reported *before* a
persistent record of the problem is made - this inevitably makes it possible
that the problem report is lost (when neither side makes a persistent record
before they crash)
	resign/no-rsp-req can be sent before PREPARE is received (implementations
with a persistent active state will typically ask for a response, those that
have no such, and don't mind if a message lost causes cancellation will not
ask for a response

THESE TABLES ARE STILL DRAFT and are part of the ongoing work of the BTP
TC - I'm circulating them to help people review the defining tables for
correctness. (The exerciser can find if the tables are inconsistent, or can
lead to an undesirable final state (e.g. contradiction where neither side
ever noticed, but it can't check if all the things that are supposed to be
allowed are allowed)

Unpack the two files to the same directory and open the tblproofindex.html
in your browser. Enjoy!

Peter

------------------------------------------
Peter Furniss
Technical Director, Choreology Ltd
email:  peter.furniss@choreology.com
phone:  +44 20 7670 1679
direct: +44 20 7670 1783
mobile: 07951 536168
13 Austin Friars, London EC2N 2JX

tables.zip