Skip to content

Commit

Permalink
Merge branch 'IntelligentEnsembles' of https://github.com/d3scomp/JDE…
Browse files Browse the repository at this point in the history 
…ECo.git into IntelligentEnsembles
  • Loading branch information
@BuckeyHack
BuckeyHack committed Feb 26, 2016
2 parents 580dcaf + a753ff5 commit 9d3e69b
Show file tree
Hide file tree
Showing 4 changed files with 78 additions and 60 deletions.
6 changes: 2 additions & 4 deletions jdeeco-edl-tests/src/cz/cuni/mff/d3s/jdeeco/edl/EDLReader.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@ public EDLReader() {
injector.injectMembers(this);
}

public EObject parse(Reader reader) {
private EObject parse(Reader reader) {
IParseResult result = parser.parse(reader);
if(result.hasSyntaxErrors())
{
Expand All @@ -35,12 +35,10 @@ public EObject parse(Reader reader) {
}

public EdlDocument readDocument(String fileName) throws IOException {
EDLReader demo = new EDLReader();

// This must be invoked before working with the model - for some reason, external model registration is done as a side-effect of accessing eInstance
cz.cuni.mff.d3s.jdeeco.edl.model.edl.EdlPackage.eINSTANCE.eClass();

EdlDocument model = (EdlDocument) demo.parse(new FileReader(fileName));
EdlDocument model = (EdlDocument) parse(new FileReader(fileName));
return model;
}
}
119 changes: 70 additions & 49 deletions ...-z3/src/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/Z3IntelligentEnsembleFactory.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,83 +37,104 @@
public class Z3IntelligentEnsembleFactory implements EnsembleFactory {

private EdlDocument ensemblesDefinition;
private Context ctx;
private Optimize opt;

public Z3IntelligentEnsembleFactory(EdlDocument ensemblesDefinition) {
this.ensemblesDefinition = ensemblesDefinition;
}

private void initConfiguration() {
HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
ctx = new Context(cfg);
opt = ctx.mkOptimize();
}

private BoolExpr[][] createAssignmentMatrix(String roleName, int maxEnsembleCount, int componentCount) {
BoolExpr[][] assignments = new BoolExpr[maxEnsembleCount][];
for (int i = 0; i < maxEnsembleCount; i++) {
assignments[i] = new BoolExpr[componentCount];
for (int j = 0; j < componentCount; j++) {
assignments[i][j] = ctx.mkBoolConst("assignment_" + roleName + "_e" + i + "_c" + j);
}
}

return assignments;
}

// assignment counters for each rescuer and train: int[#trains][#rescuers]
// assignmentTempCounters[T][0] = 0 if not assignments[T][0], otherwise 1
// assignmentTempCounters[T][R] = assignmentTempCounters[T][R-1], if not assignments[T][R], otherwise it's +1
// therefore assignmentTempCounters[T][#rescuers-1] = number of rescuers for train T
private IntExpr createCounter(BoolExpr[] assignments, int length, int index) {
ArrayExpr tempCounts = ctx.mkArrayConst("_tmp_ensemble_assignment_count_" + index, ctx.getIntSort(), ctx.getIntSort());

BoolExpr firstInSet = assignments[0];
opt.Add(ctx.mkImplies(firstInSet, ctx.mkEq(ctx.mkSelect(tempCounts, ctx.mkInt(0)), ctx.mkInt(1))));
opt.Add(ctx.mkImplies(ctx.mkNot(firstInSet), ctx.mkEq(ctx.mkSelect(tempCounts, ctx.mkInt(0)), ctx.mkInt(0))));
for (int j = 1; j < length; j++) {
BoolExpr isInSet = assignments[j];
IntExpr current = (IntExpr) ctx.mkSelect(tempCounts, ctx.mkInt(j));
IntExpr prev = (IntExpr) ctx.mkSelect(tempCounts, ctx.mkInt(j-1));
opt.Add(ctx.mkImplies(isInSet,
ctx.mkEq(current, ctx.mkAdd(prev, ctx.mkInt(1)))));
opt.Add(ctx.mkImplies(ctx.mkNot(isInSet),
ctx.mkEq(current, prev)));
}

IntExpr assignedCount = (IntExpr) ctx.mkSelect(tempCounts, ctx.mkInt(length-1));
return assignedCount;
}

@Override
public Collection<EnsembleInstance> createInstances(KnowledgeContainer container) throws EnsembleFormationException {
try {
long time_milis = System.currentTimeMillis();

initConfiguration();

Collection<Rescuer> rescuersUnsorted = container.getTrackedKnowledgeForRole(Rescuer.class);
Rescuer[] rescuers = new Rescuer[rescuersUnsorted.size()];
for (Rescuer rescuer : rescuersUnsorted) {
rescuers[Integer.parseInt(rescuer.id)-1] = rescuer;
}

HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true");
Context ctx = new Context(cfg);


EnsembleDefinition ensembleDefinition = ensemblesDefinition.getEnsembles().get(0);

RoleDefinition roleDefinition = ensembleDefinition.getRoles().get(0);

int[] positions = new int[rescuers.length];
int maxEnsembleCount = positions.length / Math.max(1, roleDefinition.getCardinalityMin());

// positions of rescuers: int[#rescuers]
/*// positions of rescuers: int[#rescuers]
IntNum[] positionExprs = new IntNum[positions.length];
for (int i = 0; i < positions.length; i++) {
positionExprs[i] = ctx.mkInt(positions[i]);
}
}*/

// assignments for each rescuer and train: bool[#trains][#rescuers]
ArrayExpr[] assignments = new ArrayExpr[maxEnsembleCount];
for (int i = 0; i < maxEnsembleCount; i++) {
assignments[i] = ctx.mkArrayConst("train_" + i, ctx.getIntSort(), ctx.getBoolSort());
}
//ArrayExpr[] assignments = createAssignmentMatrix_("rescuer", maxEnsembleCount);
BoolExpr[][] assignments = createAssignmentMatrix("rescuer", maxEnsembleCount, positions.length);

// existence of individual ensembles
BoolExpr[] ensembleExists = new BoolExpr[maxEnsembleCount];
for (int i = 0; i < maxEnsembleCount; i++) {
ensembleExists[i] = ctx.mkBoolConst("ensemble_exists_" + i);
}

Optimize opt = ctx.mkOptimize();

// assignment counters for each rescuer and train: int[#trains][#rescuers]
// assignmentTempCounters[T][0] = 0 if not assignments[T][0], otherwise 1
// assignmentTempCounters[T][R] = assignmentTempCounters[T][R-1], if not assignments[T][R], otherwise it's +1
// therefore assignmentTempCounters[T][#rescuers-1] = number of rescuers for train T
ArrayExpr[] assignmentTempCounts = new ArrayExpr[maxEnsembleCount];
IntExpr[] assignmentCounts = new IntExpr[maxEnsembleCount];
for (int i = 0; i < maxEnsembleCount; i++) {
assignmentTempCounts[i] = ctx.mkArrayConst("train_temp_count_" + i, ctx.getIntSort(), ctx.getIntSort());

BoolExpr firstInSet = (BoolExpr) ctx.mkSelect(assignments[i], ctx.mkInt(0));
opt.Add(ctx.mkImplies(firstInSet, ctx.mkEq(ctx.mkSelect(assignmentTempCounts[i], ctx.mkInt(0)), ctx.mkInt(1))));
opt.Add(ctx.mkImplies(ctx.mkNot(firstInSet), ctx.mkEq(ctx.mkSelect(assignmentTempCounts[i], ctx.mkInt(0)), ctx.mkInt(0))));
for (int j = 1; j < positions.length; j++) {
BoolExpr isInSet = (BoolExpr) ctx.mkSelect(assignments[i], ctx.mkInt(j));
IntExpr current = (IntExpr) ctx.mkSelect(assignmentTempCounts[i], ctx.mkInt(j));
IntExpr prev = (IntExpr) ctx.mkSelect(assignmentTempCounts[i], ctx.mkInt(j-1));
opt.Add(ctx.mkImplies(isInSet,
ctx.mkEq(current, ctx.mkAdd(prev, ctx.mkInt(1)))));
opt.Add(ctx.mkImplies(ctx.mkNot(isInSet),
ctx.mkEq(current, prev)));
}
assignmentCounts[i] = createCounter(assignments[i], positions.length, i);
}

// number of rescuers is 3
// number of rescuers is within cardinality conditions
for (int i = 0; i < maxEnsembleCount; i++) {
ArithExpr rescuerCount = (ArithExpr) ctx.mkSelect(assignmentTempCounts[i], ctx.mkInt(positions.length-1));
BoolExpr le = ctx.mkLe(rescuerCount, ctx.mkInt(roleDefinition.getCardinalityMax())); //!!!!!!!
BoolExpr ge = ctx.mkGe(rescuerCount, ctx.mkInt(roleDefinition.getCardinalityMin())); //!!!!!!!
BoolExpr le = ctx.mkLe(assignmentCounts[i], ctx.mkInt(roleDefinition.getCardinalityMax()));
BoolExpr ge = ctx.mkGe(assignmentCounts[i], ctx.mkInt(roleDefinition.getCardinalityMin()));
BoolExpr cardinalityOk = ctx.mkAnd(le, ge);
opt.Add(ctx.mkImplies(ensembleExists[i], cardinalityOk));
BoolExpr ensembleEmpty = ctx.mkEq(rescuerCount, ctx.mkInt(0));
BoolExpr ensembleEmpty = ctx.mkEq(assignmentCounts[i], ctx.mkInt(0));
opt.Add(ctx.mkImplies(ctx.mkNot(ensembleExists[i]), ensembleEmpty));
}

Expand All @@ -127,7 +148,7 @@ public Collection<EnsembleInstance> createInstances(KnowledgeContainer container
IntNum posExpr = ctx.mkInt(i);
BoolExpr[] assigned = new BoolExpr[maxEnsembleCount];
for (int j = 0; j < maxEnsembleCount; j++) {
assigned[j] = ctx.mkSetMembership(posExpr, assignments[j]);
assigned[j] = assignments[j][i];
}

opt.Add(ctx.mkOr(assigned));
Expand All @@ -147,24 +168,24 @@ else if (k > j)
Status status = opt.Check();
if (status == Status.SATISFIABLE) {
Model m = opt.getModel();
for (int i = 0; i < maxEnsembleCount; i++)
System.out.println("train " + i + ": " + m.getFuncInterp(assignments[i].getFuncDecl()));
for (int i = 0; i < maxEnsembleCount; i++)
System.out.println("train " + i + " temp counts: " + m.getFuncInterp(assignmentTempCounts[i].getFuncDecl()));
for (int i = 0; i < maxEnsembleCount; i++) {
System.out.print("train " + i + ": [");
for (int j = 0; j < positions.length; j++) {
System.out.print(m.getConstInterp(assignments[i][j]).getBoolValue() + " ");
}

System.out.println("]");
}

// create ensembles
List<EnsembleInstance> result = new ArrayList<>();
for (int i = 0; i < maxEnsembleCount; i++) {
IntelligentEnsemble ie = new IntelligentEnsemble(i + 1);
ie.members = new ArrayList<>();
FuncInterp fi = m.getFuncInterp(assignments[i].getFuncDecl());
Entry[] entries = fi.getEntries();
for (int j = 0; j < fi.getNumEntries(); j++) {
Expr[] a = entries[j].getArgs();
Expr v = entries[j].getValue();
for (int j = 0; j < positions.length; j++) {
Expr v = m.getConstInterp(assignments[i][j]);
if (v.getBoolValue() == Z3_lbool.Z3_L_TRUE) {
int componentId = Integer.parseInt(a[0].toString());
ie.members.add(rescuers[componentId]);
ie.members.add(rescuers[j]);
}
}

Expand Down
11 changes: 5 additions & 6 deletions ...ent-z3/test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/IntelligentEnsemblesTest.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
import java.io.ByteArrayOutputStream;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.io.IOException;
import java.io.PrintStream;
import java.io.Reader;

Expand All @@ -30,17 +31,17 @@

public class IntelligentEnsemblesTest {

public static void main(String[] args) throws InstantiationException, IllegalAccessException, DEECoException, AnnotationProcessorException, FileNotFoundException {
public static void main(String[] args) throws InstantiationException, IllegalAccessException, DEECoException, AnnotationProcessorException, IOException {
new IntelligentEnsemblesTest().testEnsembles(false);
}

@Test
@Ignore
public void testEnsembles() throws InstantiationException, IllegalAccessException, DEECoException, AnnotationProcessorException, FileNotFoundException {
public void testEnsembles() throws InstantiationException, IllegalAccessException, DEECoException, AnnotationProcessorException, IOException {
testEnsembles(true);
}

private void testEnsembles(boolean silent) throws InstantiationException, IllegalAccessException, DEECoException, AnnotationProcessorException, FileNotFoundException {
private void testEnsembles(boolean silent) throws InstantiationException, IllegalAccessException, DEECoException, AnnotationProcessorException, IOException {

ByteArrayOutputStream baos = new ByteArrayOutputStream();
if (silent) {
Expand Down Expand Up @@ -75,9 +76,7 @@ private void testEnsembles(boolean silent) throws InstantiationException, Illega

cz.cuni.mff.d3s.jdeeco.edl.model.edl.EdlPackage.eINSTANCE.eClass();

EDLReader demo = new EDLReader();
Reader reader = new FileReader("test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl");
EdlDocument model = (EdlDocument) demo.parse(reader);
EdlDocument model = (EdlDocument) new EDLReader().readDocument("test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl");

deeco.deployEnsembleFactory(new Z3IntelligentEnsembleFactory(model));

Expand Down
2 changes: 1 addition & 1 deletion ...sembles-intelligent-z3/test/cz/cuni/mff/d3s/jdeeco/ensembles/intelligent/z3/pendolino.edl
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ ensemble PendolinoEnsemble
id trainId : int
membership
roles
rescuers [3..15] : Rescuer
rescuers [6..7] : Rescuer
fitness 0

knowledge exchange
Expand Down

0 comments on commit 9d3e69b

Please sign in to comment.