These are chat archives for jdubray/sam

25th
Mar 2016
Jean-Jacques Dubray
@jdubray
Mar 25 2016 02:22
Here is the book written by Dr. Lamport on TLA+ . This is also a great reference. http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf
Jean-Jacques Dubray
@jdubray
Mar 25 2016 02:39
blob
This is the foundation of my analysis (p34) and hence the structure of SAM
HCSpec expresses both how the model mutates (next-state relation) and the next-action predicate. This is coming from the [] operator which is not available in programming languages so you need to keep them separate since they are are inherently separate.
Jean-Jacques Dubray
@jdubray
Mar 25 2016 02:44
That's an action (p21): blob
TLA+ also defines a "state function"
blob
This message was deleted
This message was deleted
Anyways, happy to have a discussion on TLA+ if anyone feels like it, as I mentioned, this is probably as close as you can get to the foundation of computing CIRCA 1990.