Time in Electrum

[keithb_b]

I cribbed from the hotel door lock example and came up with this MWE for vehicle doors.

enum LockState {Locked, Unlocked}

sig Door {
    var state: LockState
}

sig Vehicle {
     doors :  disj set Door
}

//actions
pred unlock[d: Door]{
    d.state' = Unlocked
}

pred lock[d: Door]{
    d.state' = Locked
}

//traces
pred init{
    all s: Door.state | s = Locked
}

pred trace{
    init
    always {
        some d: Door | 
            unlock[d] or
            lock[d]
    }
}

//demonstrate
run {} for 4 but exactly 2 Vehicle, 4 Time

Which to my suprise produces the instance shown here

So, I clearly don’t understand this “init” idiom, since my instance has doors in it which appear to be unlocked from the start. What am I doing wrong? Or misunderstanding.

[keithb_b]

Based on feedback from Peter over on Stack, I’ve ammended my model to the below. Which behaves as I’d like for the immediate purpose of understanding time.

As an industrial practitioner, I like examples like these which don’t do anything clever, and maybe even address a problem who’s solution offers no insight to Computer Science (!), but do clealry illustrate a technique.

And, also as a practitioner I’m finding that I tend to like quantifications which explain themsleves more than I like highly compressed relational expressions that mean the same thing but pose a puzzle. That might change, I suppose. I also like predicates with longMeanfingfulNamesEvenIfStrictlyRedundant if they help me recall what I meant when I wrote them.

enum LockState {Locked, Unlocked}

sig Door {
    var state: LockState
}

sig Vehicle {
     doors :  disj some Door
}

//actions
pred unlock[d: Door]{
    d.state' = Unlocked
}

pred lock[d: Door]{
    d.state' = Locked
}

pred unchanged[d: Door]{
    d.state = d.state'
}

//observations
pred locked[d: Door]{
    d.state = Locked
}

pred unlocked[d: Door]{
    d.state = Unlocked
}

//traces
pred begin{
    all d: Door | locked[d]
}

pred someValidChanges{
    always {
        some d: Door | 
            (unlock[d] and all dd : Door - d | unchanged[dd]) or
            (lock[d] and all dd : Door - d | unchanged[dd])
    }
}

pred targetState{
    eventually {
        all d: Door | unlocked[d]
    }
}

pred trace{
    begin
    someValidChanges
    targetState
}

//demonstrate
run {trace} for 4 but exactly 2 Vehicle, 4 Time

[steve.freeman]

I agree on the naming (my names tend to be even longer). It’s also true that it takes a while to get into the culture of a significantly different tool. Some of it is just obscurity, but some of it is what the tool is about and we have to go there. That’s how it felt learning, say, Smalltalk.

[peter.kriens]

My 2cts. It looks like you come from the developer world and seem to go through the same struggle as I am going through. So here are my personal experiences.

I was always desperately looking to apply my extensive programming knowledge & idioms so the Alloy code made sense. I over-used the quantifications because they felt so familiar as loops. But they aren’t. It is a bit like driving a plane as if it is a car.

I had not seen this message first, so as you said I answered on SO. The model I posted there was more concise. Now, this is about style issues so reasonable people can differ in opinions. One should always follow the style one is comfortable with. However, when you learn to fly, it does help to realize that you steer with your feet.

So I just like to tell the reasons why I did things differently since I tend to think very deeply about this and I am probably a few years ahead in the flying.

So this was the model I came up with (I modified the unchanged part)

enum LockState   { Locked, Unlocked }
sig Door         { var state: LockState }
sig Vehicle      { doors :  disj some Door }
pred Door.unlock { this.state' = Unlocked }
pred Door.lock   { this.state' = Locked }

pred trace {
    Door.state = Locked
    always (
        some d: Vehicle.doors {
            (d.unlock or d.lock) 
            unchanged[state,d]
        }
    )
    eventually Door.state = Unlocked
}
run trace for 4 but exactly 2 Vehicle, exactly 4 Door


pred unchanged[ relation : univ->univ, exclude : set univ ] {
  (relation -  exclude->univ)' = (relation -  exclude->univ)
}

Getters/Setters

You added ‘method’ predicates for accessing the state of a Door and keeping it unchanged. In a large program, this is really good practice. However, one of the powers of Alloy is that all values are global. I.e. you can navigate from a Door to a state

doors.state -- all states in use

But also from a state to the doors:

state.Unlocked -- all unlocked doors

Now don’t get me wrong. It took me a long time to feel that Door.state = Unlocked is identical to all d : Door | d.state = Unlocked. The second form feels so familiar. However, now I’ve learned to fly a bit, the first form is much more readable.

One could say that all d : Door | d.state = Unlocked is easier to read for newcomers but I think that is only true for newcomers from the procedural world. And they need to get the feel that Door.state = Unlocked is the same as fast as possible since it would reduce a lot of the Alloy power if you wrote models without them. I think.

By abstracting away the fields/relations I think you reduce the power of Alloy enormously. One of the hard parts of learning Alloy was for me to say goodbye to the OO model with private fields and embrace the relational model where data is completely unprotected. To understand that a relation is a global thing is something I can still struggle with.

In OO we hide our data, in Alloy (and relation) the data is what we work with. I actually also concluded in the procedural world that data is way more important than the OO gurus taught us. I work in the Java world and all these trivial getters and setter methods can drive me nuts since they rarely ever provide value.

When you use getters and setters you’re almost everywhere forced to use quantifications instead of relational. And imho worse, the name of the getters and setters cannot be trusted so to understand a model I need to look at their content. However, they most often consist a single simple Alloy expression that is often more concise and informative than a name that expresses only an intention.

For example you have

pred unchanged[d: Door]{ d.state = d.state'}

To me, d.state' = d.state screams unchanged state for that door. Actually, it tells me that only the state of the given door is unchanged, something the name does not convey to me.

I do not think that when your model grows your unlock, locked, unchanged, etc. predicates will become larger because they do not abstract anything. You cannot hide their underlying relation so you need to police your code to never use the relations directly. I think that will explode your model with predicates that are way more complex than what they abstract. The reason we use in OO of privacy and cohesion do not really apply here.

So I think it is better to stay away of the getters and the setters. In OO, the methods abstract the data. In Alloy, the data is all you got.

I tend to start with the data only. Only when I find that I repeat a non-trivial sequence of Alloy statements do I tend to put it in a predicate or function. And then as always I tried to make them reusable in multiple contexts. For example, the following unchanged method works for any relation:

 pred unchanged[ relation : univ->univ, exclude : univ ] {
     (relation -  exclude->univ)' = (relation -  exclude->univ)
}

In my mind trying to abstract the sig’s data is very much working against what makes Alloy so powerful. But your mileage may vary of course.

The reason I did not remove the lock and unlock predicates is that they are the action predicates. In my experience, they will grow in complexity over time.

OO like syntax

Not that important. However, if a predicate belongs to a type, I like to use the OO syntax. I.e.

 pred Door.lock { ... }

Instead of

 pred lock[ d : Door ] { ... }

In Alloy, they are both allowed. With the OO style syntax, there is a this keyword. Sadly you do not get an automatic resolution to the fields of names, one of my wishes is to extend the syntax to define these predicates inside the sig. Then again, it is only syntactic sugar.

Daniel doesn’t use the OO syntax in his book very often but I really like it. Because it is not in the book it is not well known.

Global/Modularity

One of the things I am still struggling with is the modularity in Alloy. In my experience so far, models tend to be quite small and most examples I’ve seen use many a fact to constrain the model.

I do not like facts since they are global, you cannot selectively enable/disable them, unlike predicates. (And there is no difference between them, they are internally identical.)

One of the reasons I tend to use predicates instead of facts is when I gradually want to explain things. Alloy has also a markdown mode when you start a file with a YAML header

This files can be edited in Alloy as markdown. Only the Alloy code blocks are given to the analyzer. This approach allows you in the run command to specify a specific predicate or provide a body.

This allows you to build up a model part by part and show run command that exercise each part separately, usually in order of complexity. However, any global fact is, well, ehh, global. If you combine modules, a stray fact can easily get in you the dreaded state of not finding a model.

That said, I’ve people tell me they don’t like it, they prefer to treat the file as their scope.

Granularity

In my model, the trace predicate contains the three predicates that you made explicit by giving them a name. It is similar to my comment on getters and setters. These predicates are rarely reusable in my experience, their only purpose is to have names. However, I need to look all over the file to find out what begin and targetState really mean since names can be wrong.

In the trace predicate the scope is clear, we’re setting up a trace. When I see:

Door.state = Locked

Then I know a lot more than when I see

begin

As a developer I applaud you but as a modeler I am always torn between the cohesive model of having a method/predicate do one thing only and the advantage of having it all visible in one place. In this case, I tend to keep them together in one predicate.

This puzzled me because I am a sucker for this cohesion rule. I think the rationale is that Alloy is so much more powerful than a programming language. A single line can do many lines of code. And if you use the proper names for the atoms and relations you can make it really readable.

Another reason might be that one of the hardest problems I experienced in Alloy is the dreaded situation that you do not get an instance. Somewhere, there is a rule that makes an instance impossible. Once you have an instance, you can use the evaluator to explore things and our mind is brilliant in seeing what is wrong.

However, that is all moot without an instance. So quite often you need to tune the model by commenting out rules and seeing how they interact. If they are all over the place, that is much harder. Another reason I tend to place them together is that these predicates are rarely reusable, they are tightly connected to where they’re called from.

Of course, when you find you need begin in lots of places and it becomes more complicated it makes sense. However, I would recommend making them parameterizable so you can control them from the trace predicate. This keeps the ‘knowledge’ of the ‘trace’ predicate local. Now you basically have 4 places that share a huge amount of knowledge. Yes, you have the names but to understand the names I need to see the code anyway because the intention they reflect might not be true (anymore). Every model will undergo a lot of tinkering and it is easy to forget to update a name. Especially long names tend to be badly maintained in my experience as a developer.

Redundancy

I was surprised you repeated handling the unchanged part for each action predicate. Imho any redundancy is going to bite. I would definitely handle that outside the actions. Any reasoning for that?

Conclusion

Again these are personal opinions so feel free to ignore. There is no best way and I’d love to see how others are addressing these issues.

[keithb_b]

Thanks for your extensive reply, but I think you may misunderstand my intent. I’m not trying to make Alloy look like Java, I’m trying to make my models read fluently. Those redundant predicates are not meant to do information hiding or encapsulation, there are there to make other predicates read more naturally. Nor are they intended to be reusable. “Design for reuse” is a scam.

You said:

These predicates are rarely reusable in my experience, their only purpose is to have names.

That’s right. That is their only purpose. Deliberately chosen. For now, I find intention revealing names a very useful pattern.

My models are going to be large and messy. I don’t know how to get paid to solve the Dining Voting Generals Problem, or whatever, in three excuisitely minimal lines. I do know how to get paid to wrangle the locking systems of motor vehicles. So I’m working towards a big, messy thing.

FYI, here’s a snap of some of my office bookshelves

I don’t prefer quantifiers because they remind me of for loops (for one thing, I detest for loops!) I prefer them becuase the read like sentences.

Yes,

Door.state = Unlocked is identical to all d : Door | d.state = Unlocked

but to me, and I strongly suspect to the folks that I’m going to show these models to, the first form is a bit of a “wait, what does that mean?” moment, and the second isn’t. All the more so in cases where the quantifers are nested two or three deep. There will be an equivalent relational expression, but for now I’m not that interested in finding it. Maybe I will come to prefer the first form, maybe not, we’ll see. But I don’t find the first form obviously strongly to be preferred in all cases.

I am aware of the “OO like” notation and in my for-real model, as opposed to Minimum Working Example models I do use it.

I’m reminded of Hal Abelson’s maxim: programs are for people to read, and only incidentally for machines to execute. So, it’s good to know about that Markdown capability, which I’ve not seen mentioned before. Why YAML?

[steve.freeman]

I found that using the evaluator helps with the transition to set-style syntax from qualifier-style, because that’s the easiest way to use it. It takes a lot of blankly staring at the prompt before it becomes fluent. Perhaps this would be a good area to provide more examples.

[peter.kriens]

Excuses if you feel misjudged This is mostly a style issue where there are no perfect answers. I just wanted to give you feedback coming from what seemed a similar area like you and recognizing some patterns. And for what it is worth, a section of my bookshelf is very similar. I think I have more Java & political books though

@keithb_b

Why YAML?

It allowed me to recognize the file as a markdown file by looking at the first 4 characters and it is well support by Github pages It is also nice to be able to specify metadata and I like the fact that you can have language-marked code blocks.

It allows me to make models, place them on Github and have them nicely formatted on a website. For example, Dining Philosopher's Problem which is maintained here: https://github.com/pkriens/pkriens.github.io/blob/master/philosophers.md

@keithb_b

I’m reminded of Hal Abelson’s maxim: programs are for people to read, and only incidentally for machines to execute.

I think there is not a lot of space in what we try to achieve, it is the how where we seem to have some differences I think

One the models I was quite proud of because it was really trying to be as readable as possible is the Knights & Knaves problem. In this problem, you have knaves always lying and knights always telling the truth. You have to figure out who is what from some expressions. In this model, I used macros to make the expressions as close as possible to the specification as I could.

enum Person { Alice, Bob, Claire, Desmond, Elena, Fernando, Gary, Horace, Ingrid }
one sig World {
	people	 : set Person,
	knights  : set people,
	knaves   : set people
} { 
	knights = people - knaves
}

let says[p,e] 	= (p) in World.knights => (e) else not (e)
let isKnave[p] 	= (p) in World.knaves
let isKnight[p] = (p) in World.knights

-- Problem 1: There are two native islanders, named Alice and Bob, 
-- standing next to each other. You do not know what type either of 
-- them is. Suddenly, Alice says “At least one of us is a Knave.”	
run BobAlice {
	World.people = Bob+Alice	

	-- Alice says: At least one of us is a Knave
	Alice.says[ some p : Bob+Alice | p.isKnave ]
}

-- Problem 2: Again, there are two native islanders standing next 
-- to each other. One is named Claire and the other is named Desmond. 
-- You do not know what type either of them are. Claire suddenly says, 
-- “We are both Knights”. After this, Desmond says “Either Claire is a 
-- Knight or I am a Knight, but we are not both Knights.

run ClaireDesmond {
	World.people = Claire+Desmond

	-- Claire says “We are both Knights”
	Claire.says[ (Claire+Desmond).isKnight ]

	-- Desmond says “Either Claire is a 
	-- Knight or I am a Knight, but we are not both Knights.
	Desmond.says[ (Claire.isKnight or Desmond.isKnight) and not ( Claire.isKnight and Desmond.isKnight ) ]
}

-- Problem 3: There are three native islanders, named Elena, Fernando, and Gary, 
-- standing together. You ask Elena, “How many knights are among you?”, and Elena 
-- answered but you couldn’t quite hear what she said. You then ask Fernando, “What 
-- did Elena say?”, and Fernando replies, “Elena said there is one knight among us.”
-- At this point, Gary says “Don’t believe Fernando; he is lying.”

run ElenaFernandoGary {
	World.people = Elena + Fernando + Gary	
	Gary.says[ not Fernando.says[ 	Claire.says[ one World.knights ] ] ]		
}

[keithb_b]

Interesting. Why don’t you have the same objection to those macros that you have to predicates used for the same purpose?

This Alloy-as-Markdown is potentially very usful. I believe you are the author? Nice work.

I find something about the way it imports modules confusing, though. See Stack.

[peter.kriens]

@keithb_b

Interesting. Why don’t you have the same objection to those macros that you have to predicates used for the same purpose?

I guess I did not make myself clear I don’t like the getter/setter’s. I like functions and predicates that take parameters. Macros are great for abstracting a concept that looks ugly when repeated.

The Knight & Knave problems uses macros because of a very subtle problem: Alloy does not have a sig for booleans. So an expression can be true or false but you cannot pass this as a parameter or store it. You need to translate it to your own boolean type. With this problem, Hillel Wayne solved it by converting the statement to its own boolean type. However, I found that it became very hard to read. By using macros, I could pass the whole expression, I did not have to turn it into a true or false enum.

My primary goal with Alloy is, is to translate an original textual specification to Alloy. Sometimes this means you need functions, predicates, or macros but in almost all cases they are parameterized to become reusable in different contexts. For me, there is a huge difference between a getter, where the actual code is more readable than a name one can never fully trust, and something like isKnave[p].

For example, for me, door.locked is less readable than door.state in Locked because I know exactly what the second form means but I will always be suspicious of the first until I looked into the predicate. That is ok if the predicate is reused in lots of places, but for this one time purpose, I’d always have to check.

I missed Alice in Wonderland in your bookshelf :-), but it contains some of my favourite lines about this topic:

"I don’t know what you mean by ‘glory,’ " Alice said.
Humpty Dumpty smiled contemptuously. “Of course you don’t—till I tell you. I meant ‘there’s a nice knock-down argument for you!’”
“But ‘glory’ doesn’t mean ‘a nice knock-down argument’,” Alice objected.
“When I use a word,” Humpty Dumpty said, in rather a scornful tone, “it means just what I choose it to mean—neither more nor less.”
“The question is,” said Alice, “whether you can make words mean so many different things.”
“The question is,” said Humpty Dumpty, “which is to be master—that’s all.”

The beauty of Alloy is that Daniel Jackson was the master …

[peter.kriens]

Yes, it took me a year to really discover the evaluator Would be nice if we could get the https://alloy.readthedocs.io/en/latest/ online and then accept contributions. Hope someone will write a nice manual for it because it is by far the best way to learn the syntax.

[DanielJackson]

Just a quick comment on the relational operators. Yes, people are more familiar with quantifiers, and that may be a reason to use them if readability by non-experts is paramount. But the reason that the relational operators are nice isn’t just that they can give you more succinct expressions. It’s that they are structural simpler, and once you’re used to reading them, they can be read more quickly and effectively. It’s like the difference between the list functionals (map/fold/reduce) and loops: certainly novices have trouble understanding the functionals, but once you’re familiar with them, they’re not only easier to understand but they eliminate a class of errors.

There is also a natural way to read many relational formulas. So I read

Door.state = Unlocked

as “the state of all doors is unlocked”. I also visualize joins as navigations. Suppose I have

sig Employee {managers: set Manager, dept: Dept}
sig Dept {head: Manager}
sig Manager extends Employee {}

Then to say that your department head must be one of your managers, I’d write

dept.head in managers

and if I had time I’d draw a little diagram with three nodes for employees, managers and departments with these expressions as two paths.

This is just a richer version of what you do when you draw Venn diagrams. You could write

all m: univ | m in Manager implies m in Employee

but once you’re familiar with sets, it’s just so much clearer to write

Manager in Employee

and to draw it as one contour inside the other.

So reserve quantifications for when there isn’t a simple relational pattern. The most common case of this arises with negations. If you want to say something like “all employees without managers must be department heads themselves” you can certainly do that without quantifiers, but it requires some skill and the result will likely be hard to read.

navigations

[DanielJackson]

I’m putting a copy of the logic chapter of my book online as I think it may help people get comfortable with the relational operators:

http://people.csail.mit.edu/dnj/teaching/alloy/logic-chapter.pdf

[alcino]

Hi,

@peter.kriens

Now don’t get me wrong. It took me a long time to feel that Door.state = Unlocked is identical to all d : Door | d.state = Unlocked . The second form feels so familiar. However, now I’ve learned to fly a bit, the first form is much more readable.

Just to clarify, these two formulas are not identical: Door.state = Unlocked can only be true if Door is not empty (if there are no doors, their state cannot be equal to unlocked), while all d : Door | d.state = Unlocked is true even if Door is empty. I think the correct relational style formula in this case would be Door.state in Unlocked.

Best,
Alcino

[alcino]

Hi,

To illustrate the usage of in in signature declaration, we could have an alternative model for the vehicle doors where, instead of using the mutable binary relation state to assign a LockState to each Door, we declare a mutable subset of Door that contains all the doors that are currently locked.

sig Door {}

var sig Locked in Door {}

sig Vehicle {
  doors :  disj some Door
}

With this change, the remainder of the model could be adapted as follows.

//actions
pred unlock[d: Door]{
    Locked' = Locked - d
}

pred lock[d: Door]{
    Locked' = Locked + d
}

//observations
pred locked[d: Door]{
    d in Locked
}

pred unlocked[d: Door]{
    d not in Locked
}

//traces
pred begin{
    Locked = Door
}

pred someValidChanges{
    always {
        some d: Door | unlock[d] or lock[d]
    }
}

pred targetState{
    eventually {
        no Locked
    }
}

pred trace{
    begin
    someValidChanges
    targetState
}

//demonstrate
run {trace} for 4 but exactly 2 Vehicle, 4 Time

Some notes:

• In the predicate someValidChanges I did not specify the frame conditions stating that all other doors remain unchanged. By stating Locked' = Locked + d in an action we are already implicitly constraining that all dd : Door - d remain unchanged (dd in Locked' iff dd in Locked). In your model you could have also specified implicitly the frame conditions in the actions by stating the global effect on the mutable relation state, instead of just saying what happens to d.state. Something like state' = state ++ d -> Locked (the ++ override operator is explained in section 3.4.3.7 of the logic chapter shared by Daniel).
• Having a set with all locked doors makes it easier to customise the theme to, for example, highlight in a different color all doors that are currently locked, making it simpler to understand traces.

Best,
Alcino

[peter.kriens]

Thanks! I never much give this much thought but this is useful. I often run into the problem that the set is empty but the quantification is true.

For a completely different thing. This discussion made me realize that maybe we should start giving sigs that are not singletons, plural names? For example:

 Doors.state = Locked

Conveys the meaning even better. I think I always name then singular because this is custom in a type system. E.g. Strings s; does feel awkward. However, a crucial part of Alloy is to realize that everything is a relation and can hold between 0 and n tuples.

Using plural for the sig names might convey this better. What do you think?

[steve.freeman]

That’s an interesting idea that makes the relational style clearer and is not bad with qualifiers: all d: Doors | d in Open

Not sure it looks as effective when used for arguments: pred unlock[d: Door]

[keithb_b]

This is a long-standing puzzle for me.

As Peter mentioned, there is a very strong convention that the name of a class, struct, or type should be singular. And there is also a very strong convention that the tables and columns in a relational database schema and the entities in an Entity-Relational model should also have singular names. On the other hand, there’s also a strong convention that the names used to refer to aggregates, such as arrays, lists and so forth, should be plural.

But, names are typically used many more times than they are defined so I’ve always had this urge to name things so that the reference sites read more naturally, even if the definition site looks a bit funky.

I’d be very relaxed to write something like this (in no particular language, but you’ll get the idea):

OrderedList<Thing> thing; //funky
// later
Thing aThing = thing.at(5) //more natural than things.at(5)

or

Dictionary<Name, Address> address;
//later
Address a = address.of(aName)

like that. I’ve met exactly one other programmer in 25 years in the industry who does not recoil in horror from this.

Now, if in sig Door the Door really is the name of the set of all…instances? rows? values? elements? of a shape, rather than being the name of the shape, then maybe they should have plural names.