How v3.0 differs from v2.0

back
open as sidenote

major changes

  • GUI and visualizer
    An improved interface and greater visualizer customizability make it easier to understand counterexamples the analyzer discovers. Details of the interface are given in the Alloy walkthrough.

  • subtypes
    The introduction of subtypes (disjoint subsets) improves clarity and efficiency, and allows more detailed specification of scopes for improved scalability. Details of how to create subtypes are given below in the descriptions of 'extends' and 'abstract'. 
      sig student extends slave {} //subtype
  sig happy in emotion {} //subset

  • atomization
    Atomization is an improvement to efficiency which is invisible to the user (although some of the new features are only possible because of it).

  • parametric polymorphism
    When you import a parametric module (such as ordering.als), you now pass it a signature name (or a comma-ed list of signature names). This replaces the old implicity polymorphism. 
      module tutorial/example
  open ordering[State]

  sig State {}
  ...

  • overloaded field names Signatures now have their own namespaces; you can declare fields in two subsignatures of a common signature that have the same name, and they will be (automatically) disambiguated by context.


  • Int
    Int is now a signature, although this does not affect the user.

    • keyword changes

  • extends --> in, extends
    If you want one signature to be a subset of another, like the old extends keyword, you now write in. If you write extends, you create subtypes instead of subsets -- subtypes are just subsets which are disjoint from each other. As a consequence, disj is no longer needed for signatures. 
      sig Person, Puppet {}

  //subsets:
  sig Happy, Ugly in Person{}

  //subtypes are disjoint subsets:
  sig Student, Faculty, Staff extends Person {}
    One of the benefits of subtypes is that you now have more control over the scope you wish to analyze. If unspecified, the scope of a subtype defaults to that of its supertype (just like subsets). However, you can also specify it manually to improce scalability of your model.

    For example, one can now write 
      check fibbles for 6 Person, 2 Staff
    and restrict Alloy to not bother examining cases where more than 2 of the Persons are Staff.

  • disj gone
    disj no longer applies to signature declarations. If you want disjoint subsets like the old disj achieved, instead create subtypes with the extends keyword.

    However, note that disj can still be used when specifying quantified variables, as in 
      all disj a,b: Foo | ...

  • abstract added
    abstract signatures have no elements/instantiations except for those that are also elements/instantiations of its subtypes. Subtypes that extend an abstract signature partition it.

    Exception: if an abstract signature has no subtypes (no signatures extend it), then the abstract keyword is ignored and it may have elements/instantiations as usual.

  • part gone
    part can no longer be written before a declaration of several signatures to indicate a partition. Instead, make the partitioning signatures subtypes (rather than subsets) using the extends keyword, and make the their supertype abstract. Thus, the old 
      sig numeral {}
  disj sig roman, arabic extends numeral {}
    would now be written 
      abstract sig numeral {}
  sig roman, arabic extends numeral {}

  • static --> one
    static is now written one, which is consistent with the way one is used as a quantifier. In both cases, it means 'exactly one'. That is, when you write one before a signature declaration, you force there to be exactly one copy of that signature. For example: 
      one Root extends Directory {}

  • fun --> fun, pred
    the old fun keyword has been split into fun, which declares a function that evalues to a value, and pred, which declares a predicate that evaluates to either true or false. That is, a function is an expression while a predicate is a formula. For example: 
      sig Widget {}

  //returns the union of the given sets
  fun InCommon (n1, n2: set Widget) : Widget {
    n1 + n2
  }

  //check that a union has been performed
  pred InCommon (n1, n2, n3: set Widget) {
    n1 + n2 = n3
  }

  • $ gone, <: and :> added
    overloading has been improved; <: and :> have replaced $.

    in general, <: anmd :> are domain restriction operators, and operate the same as in the modeling language Z.

  • with gone, @ added
    The keyword with no longer used. Add the prefix @ to preempt implicit field dereferencing in an appended fact.

  • :: changed
    :: no longer denotes relational join (.). Instead, :: replaces .. to denote a receiver for a function call. That is, x..f(y) is now written x::f(y), and makes sure that x has the same value as the expression denoted by f(y).

  • exactly added
    When specifying scopes in a run or check statement, you can say exactly. For example, 
      check Fibbles for 6 Apple, exactly 4 Orange
    will examine cases where there are up to 6 Apples and precisely 4 Oranges.

  • option, sole --> lone
    lone replaces sole as the quantifier and predicate denoting 'zero or one'. 
      fact maybe {
    lone solution
    lone s: solution | ...
  }

    Furthermore, lone replaces option in field declarations. 

      sig item {}
  sig list {
    head: item
    next: lone list
  }

  • multiplicity: +, !, ? --> some, one, lone
    The terms some, one, and lone replace the symbols +, !, and ? respectively as multiplicity markeings on relations.

  • some allowed in field declarations
    some can be in field declarations, e.g. just like set. For example, 
      sig Player {}
  sig Game {players: some Player}

  • univ, none, iden changed
    univ is now the common supertype of all atoms. there is no more univ[e] function that returns the type of the expression e.

    none is now the empty set of univ. there is no more none[e] function that returns the empty set of the type of expression e

    iden is now the identity function from univ->univ. there is no more iden[e] function that returns the identity relation over the type of e

  • exh gone
    instead of writing 
      exh a1,a2:A
    you now write 
      A in a1+a2

    The keyword part is also gone, but disj can still be used in this manner.


    • For a more detailed description of how these changed were implemented, and the benefits they provide to analysis, see the description on the Alloy website of what's new in Alloy 3.

    return to tutorial intructions

    restart the tutorial from the beginning.