HTTPS SSH

Alloy Analyzer (source code mirror by mohlerm)

Information

This is a fork of Mariachris AlloyAnalyzer on GitHub with an implementation according to the instructions given in this document: Software Architecture and Engineering 2014 Project 1. The additional code is written by Fabian Mueller and Marcel Mohler.

This analyzer takes Alloy code and translates it into C# stubs while transfering Alloy facts, predicates etc. into Code Contracts within the C# code and a test file.

Example

Input: Alloy .als file

/*  ceilings and floors */

sig Platform {}
sig Man {
  ceiling, floor: one Platform,
  between: floor -> ceiling
}

pred Above[m, n: Man] {
  m.floor = n.ceiling
}

assert BelowToo { all m: Man | one n: Man | m.Above[n] }

check BelowToo for 2 expect 1

/* dates */

sig Date {}
fun Closure[date: Date -> Date]: Date -> Date {^date}

/* genealogy */

abstract sig Person {}
sig Woman extends Person {}
one sig Eve extends Woman {}

Output: C# code file

// This C# file is generated from ..\edu\mit\csail\sdg\alloy4compiler\generator\tests0.als

#undef CONTRACTS_FULL

using System;
using System.Linq;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

public class Platform {
}

public class Man {
  public ISet<Tuple<Platform, Platform>> between;
  public Platform ceiling;
  public Platform floor;

  [ContractInvariantMethod]
  private void ObjectInvariant() {
    Contract.Invariant(between != null);
    Contract.Invariant(ceiling != null);
    Contract.Invariant(floor != null);
    Contract.Invariant(between != null && floor != null && Contract.ForAll(between, e1 => floor.Equals(e1.Item1)));
    Contract.Invariant(between != null && ceiling != null && Contract.ForAll(between, e1 => ceiling.Equals(e1.Item2)));
  }
}

public class Date {
}

abstract public class Person {
}

public class Woman : Person {
}

public class Eve : Woman {
  private static Eve instance;
  private Eve() { }
  public static Eve Instance {
    get {
      if (instance == null) {
        instance = new Eve();
      }
      return instance;
    }
  }
}

public static class FuncClass {
  public static bool Above(Man m, Man n) {
    return ((m.floor).Equals((n.ceiling)));
  }
  public static ISet<Tuple<Date, Date>> Closure(ISet<Tuple<Date, Date>> date) {
    Contract.Requires(date != null);
    Contract.Ensures(Contract.Result<ISet<Tuple<Date, Date>>>() != null);

    return Helper.Closure(date);
  }
}

public static class Helper {
  public static ISet<Tuple<L, R>> Closure<L, R>(ISet<Tuple<L, R>> set) {
    ...
  }
  public static ISet<Tuple<L, R>> RClosure<L, R>(ISet<Tuple<L, R>> set) {
    ...
  }
}

C# test file

// This C# file is generated from ..\edu\mit\csail\sdg\alloy4compiler\generator\tests0.als

using System;
using System.Linq;
using System.Collections.Generic;
using System.Diagnostics.Contracts;

public static class Test {
  public static void Main(string[] args) {
    // setup test data
    var PlatformSet = new HashSet<Platform>();
    Platform Platform0;
    PlatformSet.Add(Platform0 = new Platform());
    var ManSet = new HashSet<Man>();
    Man Man0;
    ManSet.Add(Man0 = new Man());
    Man Man1;
    ManSet.Add(Man1 = new Man());
    Man0.ceiling = Platform0;
    Man1.ceiling = Platform0;
    Man0.floor = Platform0;
    Man1.floor = Platform0;
    var DateSet = new HashSet<Date>();
    var PersonSet = new HashSet<Person>();
    Eve Eve0;
    PersonSet.Add(Eve0 = Eve.Instance);
    var WomanSet = new HashSet<Woman>();
    WomanSet.Add(Eve0);
    var EveSet = new HashSet<Eve>();
    EveSet.Add(Eve0);

    // check test data
    Contract.Assert(Contract.ForAll(ManSet, m => ManSet.Where(n => FuncClass.Above(m, n)).Count() == 1), "BelowToo");
  }
}

Summary

This is a copy of the source code for MIT's Alloy Analyzer model checking tool. It also includes an Ant build.xml script, which is not part of the original MIT source code. This copy was created to facilitate modification to the core Alloy tool (the parts which fall under the edu.mit package structure).

It was created as follows (not necessarily in this order):

  1. Downloaded the JAR file located at: http://alloy.mit.edu/alloy/downloads/alloy4.2.jar
  2. Extracted the JAR file.
  3. Added this README.md file and a build.xml file.
  4. Deleted core .class files (using the clean target in build.xml)

Building

The Ant build.xml script contains the following targets:

  • build: Compiles the .java files under the edu directory.

    Other directories are not touched; it is assumed that these contain libraries which have been pre-compiled.

    The auto-generated parser and lexer .java files (located in the edu/mit/csail/sdg/alloy4compiler/parser directory) are neither deleted nor generated by the Ant script. The directory already contains shell scripts to re-generate them using JFlex and CUP. - dist: Creates an executable JAR file in the dist directory. This JAR file looks essentially like the official Alloy JAR file released by MIT. - all: Runs dist. - clean: Deletes the dist directory and all class files under the edu directory.

Notes

  • As per the manifest, the main class is edu.mit.csail.sdg.alloy4whole.SimpleGUI.
  • The version number and build date which the tool displays are not accurate. These are set in the edu.mit.csail.sdg.alloy4.Version class, and are supposed to be updated by the build script when building a release. This project was not intended to create official releases, so it was left as-is.
  • There is a class edu.mit.csail.sdg.alloy4.MailBug which includes logic to email crash reports to MIT. You should change this class if you are modifying the source code and creating your own release.