These are chat archives for jdubray/sam

15th
Mar 2016
Jean-Jacques Dubray
@jdubray
Mar 15 2016 08:42
Comparing Hot JavaScript Frameworks: AngularJS, Ember.js and React.js http://www.infoq.com/presentations/comparing-angular-ember-react#.VufIQfGNwow.twitter
Jean-Jacques Dubray
@jdubray
Mar 15 2016 08:54
blob
blob
weepy
@weepy
Mar 15 2016 09:01
so one question --- I've read about TLA+ that you mention a lot, but I'm not really quite sure on the link between them ? Is there something more rigorous ?
Jean-Jacques Dubray
@jdubray
Mar 15 2016 09:17
All I can offer is the posts I wrote while trying to understand TLA+
I exchanged several emails with Dr Lamport to discuss my understanding

Basically his point is:

State machines can be described and manipulated with ordinary, everyday mathematics—
that is, with sets, functions, and simple logic.

as opposed to the traditional <Si,A,Si+1>
I found this tutorial to be the most approachable; http://tla2014.loria.fr/slides/merz.pdf
see section 3.1 slide 40 ->
Jean-Jacques Dubray
@jdubray
Mar 15 2016 09:35
blob
This is how you model a system in TLA+
Model -> VARIABLES i,o,q
Actions -> LQEnq, LQDeq
This system does not have automatic actions
This is the equivalent of S(), but there is of course no concept of "State Representation" in TLA+ LQNext ( LQEnq∨LQDeq )
Jean-Jacques Dubray
@jdubray
Mar 15 2016 09:43
SAM does not prescribe how the system is initialized, because SAM is not a system specification but a pattern, it is only interested in how to structure the elements of the system.
You may also want to read about Praxos: https://en.wikipedia.org/wiki/Paxos_(computer_science)