Should this be a fact? It seems more like a predicate that you’d check as a spec property.
some s.undefined => {
// If there are machines in an undefined state then they
// must move to the new state but they don't all have to
// move together
some (s.undefined & s'.new)
// We don't specify what is happening to the old machines.
// Think about why this is ok (or not).
}
I think this allows rollbacks, ie s.undefined & s'.old. Is that something you intended?
Given the disjointness condition and s.new in s'.new at the top we avoid rollbacks because it forces new to be a monotone relation relative to the state order, i.e. as soon as a machine is in a new state it stays in a new state.
But that probably means I could be more clear with the transition relation to make that more obvious.
Edit: Oh I see what you mean. I translated “rollback” as moving from new to old and then realized what you meant. I’ll have to think about that. I remember having something along those lines in a previous iteration that I took out but I don’t remember why. Shoulda kept better notes.
I’m throwing in a davidk01 quote about how to use Alloy from another thread in case anyone finds it interesting. If I try to learn it, I wondered how I’d get used to expressing things in its simplistic logic. Any such logic might be weird to programmers without logic background. davidk01 surprises me saying he uses it like SQL:
“When I’m writing Alloy specs I just pretend I have tables and I can query those tables with SQL and various extensions like recursive CTEs. Once I have a sketch of a potential solution in SQL-pseudo-code I refine it in Alloy by translating the table/SQL based mental model into Alloy syntax. This goes a surprisingly long way because I think it is a really good first order approximation. If you know SQL then you can definitely learn enough Alloy to get by without having to learn the underlying logic.
For learning resources I’m not sure what I can recommend. I don’t think the meta-theory of the underlying logic is that important for Alloy specs if you have a good enough approximation of it. Pretending Alloy is SQL hasn’t led me astray yet.”
I think knowing that can work might suddenly make Alloy seem much more approachable and potentially useful to readers here based on experiences with SQL. @hwayne, what do you think about the SQL and Alloy view? And did you find any similar heuristics to getting more use out of it without being a logician or something?
Should this be a fact? It seems more like a predicate that you’d check as a spec property.
I think this allows rollbacks, ie
s.undefined & s'.old. Is that something you intended?Given the disjointness condition and
s.new in s'.newat the top we avoid rollbacks because it forcesnewto be a monotone relation relative to the state order, i.e. as soon as a machine is in a new state it stays in a new state.But that probably means I could be more clear with the transition relation to make that more obvious.
Edit: Oh I see what you mean. I translated “rollback” as moving from
newtooldand then realized what you meant. I’ll have to think about that. I remember having something along those lines in a previous iteration that I took out but I don’t remember why. Shoulda kept better notes.I’m throwing in a davidk01 quote about how to use Alloy from another thread in case anyone finds it interesting. If I try to learn it, I wondered how I’d get used to expressing things in its simplistic logic. Any such logic might be weird to programmers without logic background. davidk01 surprises me saying he uses it like SQL:
“When I’m writing Alloy specs I just pretend I have tables and I can query those tables with SQL and various extensions like recursive CTEs. Once I have a sketch of a potential solution in SQL-pseudo-code I refine it in Alloy by translating the table/SQL based mental model into Alloy syntax. This goes a surprisingly long way because I think it is a really good first order approximation. If you know SQL then you can definitely learn enough Alloy to get by without having to learn the underlying logic.
For learning resources I’m not sure what I can recommend. I don’t think the meta-theory of the underlying logic is that important for Alloy specs if you have a good enough approximation of it. Pretending Alloy is SQL hasn’t led me astray yet.”
I think knowing that can work might suddenly make Alloy seem much more approachable and potentially useful to readers here based on experiences with SQL. @hwayne, what do you think about the SQL and Alloy view? And did you find any similar heuristics to getting more use out of it without being a logician or something?