00001
00005 package edu.mit.csail.sdg.squander.examples.partitioning;
00006
00007 import java.util.HashSet;
00008 import java.util.Set;
00009
00010 import edu.mit.csail.sdg.annotations.Ensures;
00011 import edu.mit.csail.sdg.annotations.Invariant;
00012 import edu.mit.csail.sdg.annotations.Modifies;
00013 import edu.mit.csail.sdg.squander.Squander;
00014 import edu.mit.csail.sdg.squander.annotations.Fresh;
00015 import edu.mit.csail.sdg.squander.annotations.FreshObjects;
00016 import edu.mit.csail.sdg.squander.annotations.Options;
00017 import edu.mit.csail.sdg.squander.engine.ISquanderResult;
00018 import edu.mit.csail.sdg.squander.log.Log.Level;
00019 import edu.mit.csail.sdg.squander.options.GlobalOptions;
00020
00021 @Invariant({
00022
00023 "null !in this.parts.elts + this.doms.elts + this.lits.elts",
00024
00025
00026 "all p : this.parts.elts | p.doms.elts in this.doms.elts",
00027 "all d : this.doms.elts | d.insts.elts in this.lits.elts",
00028
00029
00030 "all d : this.doms.elts | d in this.parts.elts.doms.elts",
00031
00032
00033 "all p1 : this.parts.elts| all p2 : this.parts.elts | p1 != p2 => p1.doms.elts != p2.doms.elts",
00034
00035
00036 "all lit : this.lits.elts | one d : this.doms.elts | lit in d.insts.elts"
00037 })
00038 public class Graph {
00039
00040 private static final int n = 4;
00041
00042 private final Set<Partition> parts = new HashSet<Partition>();
00043 private final Set<Domain> doms = new HashSet<Domain>();
00044 private final Set<Literal> lits = new HashSet<Literal>();
00045
00046 @Ensures({
00047 "some this.parts.elts",
00048 "some this.doms.elts",
00049 "some this.lits.elts",
00050 "#this.parts.elts > #this.doms.elts",
00051 "#this.doms.elts < #this.lits.elts"
00052 })
00053 @Modifies({
00054 "this.parts.elts",
00055 "this.doms.elts",
00056 "this.lits.elts",
00057 "Partition.doms.elts",
00058 "Domain.insts.elts"
00059 })
00060 @Fresh({
00061 @FreshObjects(cls=Partition.class, num = n),
00062 @FreshObjects(cls=Domain.class, num = n),
00063 @FreshObjects(cls=Literal.class, num = n)
00064 })
00065 @Options(solveAll = true)
00066 public void gen() {
00067 Squander.exe(this);
00068 }
00069
00070 @Override
00071 public String toString() {
00072 StringBuilder sb = new StringBuilder();
00073 sb.append(String.format("Partitions: %s\n", parts.toString()));
00074 sb.append(String.format("Domains: %s\n", doms.toString()));
00075 sb.append(String.format("Literals: %s\n", lits.toString()));
00076 sb.append("-----------------------------------------------\n");
00077 sb.append(String.format("partition -> {domain}:\n"));
00078 for (Partition p : parts) {
00079 sb.append(String.format(" %s -> %s\n", p, p.getDoms()));
00080 }
00081 sb.append("\n");
00082 sb.append(String.format("domain -> {literal}:\n"));
00083 for (Domain d : doms) {
00084 sb.append(String.format(" %s -> %s\n", d, d.getInsts()));
00085 }
00086 return sb.toString();
00087 }
00088
00089 public static void main(String[] args) {
00090 Graph g = new Graph();
00091 GlobalOptions.INSTANCE.log_level = Level.NONE;
00092 g.gen();
00093 while (true) {
00094
00095
00096
00097 try {
00098 ISquanderResult r = Squander.getLastResult();
00099 if (r.hasSolution()) {
00100
00101 r.findNext();
00102 } else {
00103 break;
00104 }
00105 } catch (Throwable t) {
00106 System.out.println("no more solutions");
00107 t.printStackTrace();
00108 break;
00109 }
00110 }
00111 }
00112 }