TLA+-like unchanged

1

Hey All,

I’m trying to create a TLA±like unchanged function, but there are two problems that I seem to be having.

module unchanged[x]

pred unchanged[s:x]{
	s' = s
}

The first, is that I can’t seem to pass relationships as signatures like
open unchanged[file->directory] or open unchanged[file.directory]

How do pass a relationship as a parameter in a generic function?

Second, is there a way to have variadic functions? For instance, if I wanted to have a stutter action for several variables, I need to do the following:

    unchanged[set1]
    unchanged[set2]
    unchanged[set3]

but what I really want is:

    unchanged[set1,set2,set3]
2

I suppose you meant generic module. It’s not possible. In my view, a richer module system for Alloy could have some benefits.

BUT, you can nonetheless create a unique unchanged macro (macros are a little documented extension introduced in Alloy 4):

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

Macros are brittle and prime should apply to all of r so I add parentheses.

No. I also asked for them recently but I think it’s not in sight :slight_smile:
The meta capabilities of Alloy are however going to be fixed and extended in the forthcoming version, which could help write some predicates applying to various objects at once. Proper variadic predicates or macros will not be available however.

1 Like
3

You weren’t kidding when you said they were brittle. I ended up using the definition in multiple modules, and immediately ran into issues. I then tried to then have a single definition, like in the lowest module (thing file like in a file, directory, os hierarchy.

Name cannot be resolved; possible incorrect
function/predicate call; perhaps you used ( ) when you
should have used [ ]
4

Strange. Can you give a minimal working example?

1 Like
5

I found the problem, while trying to make a minimal example.

First, I was calling a field by it’s type and not by its name.
Second, I was calling an object that was unreachable in the module (in a higher layer)