Alloy error signature

Question

Your primary problem is that the second edition of the Huth / Ryan book appears to have been published in 2004 and to use (unsurprisingly) the syntax accepted by the Alloy Analyzer at that time, which is (also unsurprisingly) not quite the same as the syntax accepted by current versions of the Alloy Analyzer.

So to run this in a current version of the Analyzer, you are going to have to understand (a) what they are trying to say (b) the then-current Alloy syntax in which they are trying to say it, and (c) the current Alloy syntax, well enough to translate the model into current syntax. (Or else find someone who has done this already.) Fortunately, Huth and Ryan explain the Alloy syntax they use in some detail, so it's not a difficult exercise for someone familiar with Alloy 4 to translate the model into the Alloy 4 syntax.

Good luck!

[Postscript] On the theory that the goal of your assignment is to let you get familiar with the Alloy Analyzer, and not to drop you in the deep end by requiring a translation from the old Alloy syntax to the new Alloy syntax, I append a rough translation of the Huth / Ryan PDS model into Alloy 4 syntax, with some interspersed comments. (I say 'rough' because I haven't spent a lot of time on it, and I may have missed some nuances, especially in the predicate HighestVersionPolicy, where the authors get a little tricky.) If the goal of your assignment is precisely to force you to fight your way through the thickets of syntax with only your native ingenuity to use as a machete, then I apologize for messing up that experience.

At the top of the module, the main change is to the way the ordering library module is invoked.

module PDS

open util/ordering[Number]

In Component, the keyword 'option' is replaced by the current keyword 'lone', and I've transcribed some of Huth and Ryan's comments, to try to help myself understand what is going on better.

sig Component {
    name: Name, // name of the component
    main: lone Service, // component may have a 'main' service
    export: set Service, // services the component exports
    import: set Service, // services the component imports
    version: Number  // version number of the component
}{ 
   no import & export // imports and exports are disjoint 
                      // sets of services
}

In the sig for PDS, the main change is again the change to cardinality syntax: ->? becomes -> lone.

// Package Dependency System
// components is the set of Component in this PDS
// schedule assigns to each component in the PDS
//   and any of its import services 
//   a component in the PDS that provides that service
//   (see SoundPDSs, below)
// requires expresses the component dependencies
//   entailed by the schedule
sig PDS {
    components: set Component,
    schedule: components -> Service ->  lone components,
      // any component / Service pair maps to at most
      // one component
    requires: components -> components
}{ 
    // for every component in the system,
    // the services it imports are supplied (exported)
    // by some (other) component in the system
    components.import in components.export 
}

In the fact SoundPDSs, the authors use a with P construct which I don't remember ever seeing in versions of Alloy I've used. So I took it out, and reformulated the expressions a bit for clarity, since the authors explain that clarity is their main motive for using the with P construct. It will be well worth your while to be sure you understand Alloy's box notation, and why P.schedule[c][s] is another way of writing c.(P.schedule)[s] or s.(c.(P.schedule)).

fact SoundPDSs {
  all P : PDS | {
    all c : P.components, s : Service |
      let c' = P.schedule[c][s] {
        (some c' iff s in c.import)
        // c and s require c' only iff c imports s
        &&
        (some c' => s in c'.export)
        // c and s require c' only if c' exports s
      }
    all c : P.components | P.requires[c]= P.schedule[c][Service] 
    // c requires precisely those components
    // that schedule says c depends on for some service
  }
}

sig Name, Number, Service {}

The big change from here on out is that Huth and Ryan use fun for their definitions of various properties, where Alloy 4 uses pred -- the keyword fun is still legal, but it means a function (an expression which when evaluated returns a value, not a Boolean) not a predicate.

pred AddComponent(P, P': PDS, c: Component)  {
    not c in P.components
    P'.components = P.components + c
} run AddComponent for 3 but 2 PDS

pred RemoveComponent(P, P' : PDS, c: Component) {
    c in P.components
    P'.components = P.components - c
} run RemoveComponent for 3 but 2 PDS

In HighestVersionPolicy, I've again introduced box notation to try to make the expression clearer. Note that prev is not defined here -- it's one of the relations imported by the import instruction (open ...) at the top of the module, from the library module for ordering.

pred HighestVersionPolicy(P: PDS) {
    all s : Service, 
        c : P.components, 
        c' : P.schedule[c][s],
        c'' : P.components - c' {
            s in c''.export && c''.name = c'.name 
            => 
            c''.version in ^prev[c'.version]
        }
} run HighestVersionPolicy for 3 but 1 PDS

pred AGuideSimulation(P, P', P'' : PDS, c1, c2 : Component) {
    AddComponent[P, P', c1] 
    RemoveComponent[P, P'', c2]
    HighestVersionPolicy[P] 
    HighestVersionPolicy[P']    
    HighestVersionPolicy[P'']
} run AGuideSimulation for 3

assert AddingIsFunctionalForPDSs {
    all P, P', P'' : PDS, c : Component {
        AddComponent[P, P', c] && AddComponent[P, P'', c] 
        => P' = P''
    }
}

check AddingIsFunctionalForPDSs for 3

The version of their model given by Huth and Ryan on the web doesn't include the StructurallyEqual predicate they describe in their text; I added it to help make sure my translation of the model worked.

pred StructurallyEqual(P, P' : PDS) {
  P.components = P'.components
  P.schedule = P'.schedule
  P.requires = P'.requires
}

run StructurallyEqual for 2

And similarly, they don't include the fix to AddingIsStructurallyFunctional -- the intent is presumably for the student to do it dynamically, in Alloy.

assert AddingIsStructurallyFunctionalForPDSs {
    all P, P', P'' : PDS, c : Component {
        AddComponent[P, P', c] && AddComponent[P, P'', c] 
        => 
        StructurallyEqual[P',P'']
    }
}
check AddingIsStructurallyFunctionalForPDSs for 3