Alloy 6 vs. TLA+

Alloy 6
21

Coming back to this thread after doing what turned out to be a massive project in Alloy 6, I think I need to share some thoughts.

The project I worked on was specifically a series of work flows that enable a factory, and customer service technicians to get credentials for a new or serviced machine, by using a unique hardware identifier.

Alloy 6 had some very charming features, but also some very nasty drawbacks that make it jarring to work with.

Let’s open up with the nice features.

The big one is being able to effectively roll the dice and see many different structural combinations that are allowed in a given model. This highlighted about 60% of the problems we were going to run into.

Second, being able to use set theory to describe the various states of the machines, the sub component which stores the unique hardware identifier, and the types of mappings of connections to our backend found the next 30% of problems.

It can kinda model time with actions. This found the last 10% of problems that needed to be addressed.

There are some other nice features that are a little weird, like being able to describe “all the other machines” as machine - m where m is the machine the current function is applied to.

The pain points:

Specificity. Unlike TLA+, Alloy can’t tell you when you’re a variable or a mapping is being implicitly left to changed. In a massive system that spans across multiple machines, sub component, production facilities, and end users locations (gyms), you need to pathologically specify each step. With large numbers of variables and mappings that means lots unchanged or stuttering sets, in frankly a poorly scalable method. I also have the expectation that stuttering a machine would stutter it’s fields as well, but that’s not the case at all.

Lists. Without a language level list, this only exacerbates the previous issue, in so far, 40% of my specifications are just stutter and unchanged lines, of various flavors to lock down what’s modified.

Sub-sets. Things get real funky when describing what happens with sub-sets. I would expect that a subset of machine (e.g. powered_on machines) would also be stuttered if I stuttered it’s superset.

Now, would I be able to implement the same specification in TLA+? I don’t know, this project was more interested in the implicit structures that could be formed across machines and services, and that would’ve been very difficult in TLA+. However, modeling actions was frankly pulling teeth, and I would really hate to extend my model further.

In summary: I still think Alloy is good for structural studies, but I think it’s inappropriate for adoption of industry as a whole, especially with temporal studies or with verification.

2 Likes
22

I don’t understand some of your points. Without seeing a representative example of your model, we can’t see whether there would have been a solution to the issues you encountered. We can’t assess whether Alloy and TLA+ are the best approaches in this context. We can’t compare Allow and TLA+ solutions to the same problem. We don’t which temporal properties you want to check.

A few remarks:

  • Alloy does have lists in the shape of sequences.
  • Regarding the specification of steps, TLA+ asks that you specify unchanged variables (the advantage is that UNCHANGED can take a tuple as parameter).
  • Regarding “machines”, which do not exist in Alloy per se, you could perhaps specify that some variables don’t change when one (representing a machine) doesn’t.
23

Here is a minimal case necessary to start showing pain points.

let unchanged[c] { ( c = (c)' ) }

var sig microProc{}

var sig machine {
    var uP : lone microProc,
    var cached_uP: lone microProc
}

var sig powered in machine{}
var sig online in powered{}

one sig backend{
	var entries : machine -> lone microProc 
}

pred stutter_machines[m :set machine]{
	// Preserve that devices don't switch membership spontaneously
	all i : m | unchanged[i] and unchanged [i.uP] and unchanged[i.cached_uP]
	// Maintain membership in these groups
	unchanged[m]
	unchanged[m.uP]
	unchanged[m.cached_uP]
}

pred backendDelete[m:machine, c:uP]{
	some backend.entries[m]
	backend.entries' = backend.entries - (m -> c)
	unchanged[uP]
	stutter_machines[machine]
	stutter_machines[online]
	stutter_machines[powered]
}

This becomes onerous at scale. What I would expect is something like:

pred backendDelete[m:machine, c:uP]{
	some backend.entries[m]
	backend.entries' = backend.entries - (m -> c)
	unchanged[machine]
}

Effectively locking the superset of machine ST items within machine do not change their membership, and nor do their fields change membership. This would already alleviate the problem that I was facing with lists.

Even at the lowest level, the following would be a big improvement in QoL:

pred stutter_machines[m :set machine]{
	// Preserve that devices don't switch membership spontaneously
	all i : m | unchanged[i, i.uP, i.cached_uP]
	// Maintain membership in these groups
	unchanged[m, m.uP, m.cached_uP]
}
24

Thanks, i can’t really comment right now but will come back to this late August.

25

Hi,

I don’t agree that should be the semantics in general. I can think of examples where I might want to keep a superset unchanged but change a subset. Like @grayswandyr mentioned, if you want that particular semantics in your example you can just add a fact stating precisely that, for example something like:

fact machine_stuttering {
	always (unchanged[machine] implies unchanged[uP] and unchanged[cached_uP] and unchanged[powered] and unchanged[online])
}

Now if you want to keep all machines and machine subsets unchanged in a particular event you only need to state unchanged[machine], for example:

pred backendDelete[m:machine, c:microProc]{
	some backend.entries[m]
	backend.entries' = backend.entries - (m -> c)
	unchanged[machine]
}

Btw, in your predicate stutter_machines I think you have some redundant constraints and that it could be simplified to:

pred stutter_machines[m :set machine]{
	unchanged[m]
	unchanged[m <: uP] 
	unchanged[m <: cached_uP] 
}

Best,
Alcino

2 Likes
26

Hey Alcino,

Thanks for the tip using the domain restriction.

Alex