+ private void constructminsizes() {
+ boolean change=true;
+ HashSet usedsources=new HashSet();
+ while (change) {
+ change=false;
+ for(int i=0;i<state.vRules.size();i++) {
+ Rule r=(Rule)state.vRules.get(i);
+ //model defition rule with no condition
+ if ((!(r.getGuardExpr() instanceof BooleanLiteralExpr))||
+ (!((BooleanLiteralExpr)r.getGuardExpr()).getValue()))
+ continue;
+ //inclusion condition needs to be safe
+ if ((!(r.getInclusion() instanceof SetInclusion))||
+ (!((SetInclusion)r.getInclusion()).getExpr().isSafe()))
+ continue;
+ //needs exactly 1 quantifier which is a set quantifier
+ if (r.numQuantifiers()!=1||
+ (!(r.getQuantifier(0) instanceof SetQuantifier)))
+ continue;
+ SetQuantifier sq=(SetQuantifier)r.getQuantifier(0);
+ SetDescriptor sd=sq.getSet();
+ int size=-1;
+ Constraint source=null;
+ if (getsize(sd)>0) {
+ size=getsize(sd);
+ source=getConstraint(sd);
+ } else if (minSize(sd)>0) {
+ size=minSize(sd);
+ source=ensuresMinSize(sd);
+ } else continue;
+ if (size>1)
+ size=1; //would need more in depth analysis otherwise
+ SetDescriptor newsd=((SetInclusion)r.getInclusion()).getSet();
+ if (usedsources.contains(newsd))
+ continue; //avoid dependence cycles in our analysis
+ //need to force repair to fix one of the constraints in the cycle
+ int currentsize=minSize(newsd);
+ if (size>currentsize) {
+ SizeObject so=new SizeObject(newsd);
+ minsize.put(so, new Integer(size));
+ constraintensureminsize.put(so,source);
+ usedsources.add(source);
+ System.out.println("Set "+newsd.toString()+" has minimum size "+size);
+ change=true;
+ //need update
+ }
+ }
+ }
+ }
+