Why would prime (aka ') raise an error in the following: pred add (b, b': Book, n: Name, a: Addr) { b’.addr = b.addr + n -> a }?

user_10497996 0
Viewed 38
  • I have Alloy 6.1.0 running on Windows 10
  • I have "Software Abstractions" text by Daniel Jackson and working through book.
  • I am at the examples in the "Whirlwind Tour" and section 2.2 "Dynamics: Adding Operations".
  • Verbatim from the book I have coded up the following:
    module tour/addressBook1
    
    sig Name, Addr {}
    sig Book {
      addr: Name -> lone Addr
    }
    
    pred show (b: Book) {
    #b.addr >1
    #Name.(b.addr) > 1
    }
    
    pred add (b,b': Book, n: Name, a: Addr) {
    b'.addr = b.addr + n -> a
    }
    
    run add for 3 but 2 Book

Results in:

Syntax error at line 13 column 14:
There are 3 possible tokens that can appear here:
, : =

Against the prime (') in

pred add (b,b': Book, ...

I understand the version of Alloy in the book will be behind the one I am using, but surely prime is still a thing, so it isn't ituitive why I am getting this syntax error.

Is there a module I need load nowadays?

I have also jumped ahead to Figure 2.7 and just snipped the full model out, rather than use my hand coded attempts. Same error at the same point.

alloy
1 Answers

Good question, Asterion! As you suspected, the prime symbol is now special in Alloy 6, with the addition of the new temporal features from Electrum. So you'll need to use a different symbol to run the examples from the book. Sorry about this. It's the one cost of the lovely new temporal features.

user_15470460
Related