Added annotations to examples

examples/kodkod/examples/ExampleMetadata.java

@@ -0,0 +1,57 @@
+package kodkod.examples;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.RUNTIME)
+@Target(ElementType.TYPE)
+public @interface ExampleMetadata {
+    // example name
+    String Name() default "";
+
+    // example note
+    String Note() default "";
+
+    // "check" or "run"
+    boolean IsCheck() default false;
+
+    // partial models
+    boolean PartialModel() default false;
+
+    // decidable fragments, satisfiability with finite extension
+    // TODO
+
+    // number of binary, ternary, and n-ary relations
+    int BinaryRelations() default 0;
+    int TernaryRelations() default 0;
+    int NaryRelations() default 0;
+
+    // number of hierarchical types
+    int HierarchicalTypes() default 0;
+
+    // number of nested relational joins
+    int NestedRelationalJoins() default 0;
+
+    // number of transitive closure
+    int TransitiveClosure() default 0;
+
+    // number of nested quantifiers
+    int NestedQuantifiers() default 0;
+
+    // set cardinality
+    int SetCardinality() default 0;
+
+    // number of additions and subtractions
+    int Additions() default 0;
+    int Subtractions() default 0;
+
+    // number of comparison operators
+    int Comparison() default 0;
+
+    // number of ordered relations
+    int OrderedRelations() default 0;
+
+    // number of constraints
+    int Constraints() default 0;
+}

examples/kodkod/examples/alloy/AbstractWorldDefinitions.java

@@ -13,6 +13,7 @@
 import kodkod.engine.Solver;
 import kodkod.engine.config.ConsoleReporter;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.Universe;
@@ -22,6 +23,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "AbstractWorldDefinitions",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 4,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 4,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 14,
+		OrderedRelations = 0,
+		Constraints = 54
+)
 public final class AbstractWorldDefinitions {
 	// relations declared in common.als
 	private final Relation Coin, Purse, TransferDetails;

examples/kodkod/examples/alloy/Bigconfig.java

@@ -12,6 +12,7 @@
 import kodkod.engine.Solver;
 import kodkod.engine.config.ConsoleReporter;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -57,6 +58,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "Bigconfig",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 2,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 2,
+		NestedRelationalJoins = 2,
+		TransitiveClosure = 1,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 0,
+		OrderedRelations = 0,
+		Constraints = 9
+)
 public class Bigconfig {
 //	 sigs
 	private final Relation Router, Site, HQ, Sub;

examples/kodkod/examples/alloy/CeilingsAndFloors.java

@@ -9,6 +9,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.Universe;
@@ -55,6 +56,25 @@
  * </pre>
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "CeilingsAndFloors",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 2,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 0,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 5,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 4,
+		OrderedRelations = 0,
+		Constraints = 7
+)
 public final class CeilingsAndFloors {
 	private final Relation Platform, Man, ceiling, floor;
 

examples/kodkod/examples/alloy/DNACuts.java

@@ -11,6 +11,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -70,6 +71,25 @@
  * </pre>
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "DNACuts",
+		Note = "",
+		IsCheck = false,
+		PartialModel = false,
+		BinaryRelations = 3,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 6,
+		NestedRelationalJoins = 2,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 9,
+		OrderedRelations = 1,
+		Constraints = 11
+)
 public final class DNACuts {
 	private final Relation next, Link, CutLink, JoinLink, Base, base, partner;
 	private final Expression[] neighbor;

examples/kodkod/examples/alloy/DiffEg.java

@@ -9,6 +9,7 @@
 import kodkod.ast.Variable;
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.Universe;
@@ -36,6 +37,25 @@ pred pol (req: Request) {
 
 run pol for 2
 */
+@ExampleMetadata(
+		Name = "DiffEg",
+		Note = "",
+		IsCheck = false,
+		PartialModel = false,
+		BinaryRelations = 5,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 0,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 0,
+		OrderedRelations = 0,
+		Constraints = 8
+)
 public final class DiffEg {
 //	 sigs
 

examples/kodkod/examples/alloy/Dijkstra.java

@@ -11,6 +11,7 @@
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.TupleSet;
@@ -20,6 +21,25 @@
  * Kodkod encoding of models/examples/algorithms/dijkstra.als.
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "Dijkstra",
+		Note = "",
+		IsCheck = true,
+		PartialModel = false,
+		BinaryRelations = 2,
+		TernaryRelations = 2,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 28,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 1,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 12,
+		OrderedRelations = 2,
+		Constraints = 33
+)
 public final class Dijkstra {
 
 	private final Relation Process, Mutex, State, holds, waits;

examples/kodkod/examples/alloy/FileSystem.java

@@ -15,6 +15,7 @@
 import kodkod.engine.fol2sat.HigherOrderDeclException;
 import kodkod.engine.fol2sat.UnboundLeafException;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.Universe;
@@ -23,6 +24,25 @@
  * A KK encoding of file_system.als
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "FileSystem",
+		Note = "",
+		IsCheck = true,
+		PartialModel = true,
+		BinaryRelations = 4,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 4,
+		NestedRelationalJoins = 2,
+		TransitiveClosure = 2,
+		NestedQuantifiers = 3,
+		SetCardinality = 0,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 4,
+		OrderedRelations = 0,
+		Constraints = 10
+)
 public final class FileSystem {
 
 	private final Relation Obj, Name, File, Dir, Root, Cur, DirEntry;
@@ -200,7 +220,7 @@ public  static void main(String[] args) {
 		} catch (UnboundLeafException e) {
 			// TODO Auto-generated catch block
 			e.printStackTrace();
-		} 
+		}
 	}
 
 }

examples/kodkod/examples/alloy/GroupScheduling.java

@@ -34,6 +34,7 @@
 import kodkod.engine.Solver;
 import kodkod.engine.config.ConsoleReporter;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.Tuple;
 import kodkod.instance.TupleFactory;
@@ -46,6 +47,25 @@
  * @author Emina Torlak
  *
  */
+@ExampleMetadata(
+		Name = "GroupScheduling",
+		Note = "",
+		IsCheck = false,
+		PartialModel = true,
+		BinaryRelations = 0,
+		TernaryRelations = 1,
+		NaryRelations = 0,
+		HierarchicalTypes = 0,
+		NestedRelationalJoins = 2,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 1,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 1,
+		OrderedRelations = 0,
+		Constraints = 3
+)
 public final class GroupScheduling {
 	private final Relation person, group, round, assign;
 	private final int ng;

examples/kodkod/examples/alloy/Handshake.java

@@ -11,6 +11,7 @@
 import kodkod.engine.Solver;
 import kodkod.engine.config.ConsoleReporter;
 import kodkod.engine.satlab.SATFactory;
+import kodkod.examples.ExampleMetadata;
 import kodkod.instance.Bounds;
 import kodkod.instance.TupleFactory;
 import kodkod.instance.Universe;
@@ -20,6 +21,25 @@
  * 
  * @author Emina Torlak
  */
+@ExampleMetadata(
+		Name = "Handshake",
+		Note = "",
+		IsCheck = false,
+		PartialModel = true,
+		BinaryRelations = 2,
+		TernaryRelations = 0,
+		NaryRelations = 0,
+		HierarchicalTypes = 2,
+		NestedRelationalJoins = 1,
+		TransitiveClosure = 0,
+		NestedQuantifiers = 0,
+		SetCardinality = 2,
+		Additions = 0,
+		Subtractions = 0,
+		Comparison = 9,
+		OrderedRelations = 0,
+		Constraints = 10
+)
  public final class Handshake {
 	private final Relation Person, Hilary, Jocelyn, shaken, spouse;