Commit bb60db95 authored by MALLET Frederic's avatar MALLET Frederic

Fix Issue #1 and #2

intermediate clocks were not propagated to ClockCollector when unfolding
ternary expressions like inf or sup.
Fix semantics of implies to implies union of clocks, we can add more
constraints to mean implies intersection of clocks
parent 23162115
......@@ -4,11 +4,7 @@ import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import fr.kairos.timesquare.ccsl.IDefinition;
import fr.kairos.timesquare.ccsl.IRelation;
import fr.kairos.timesquare.ccsl.ISpecification;
final class ClockCollector implements ISpecification, Iterable<IClock>, INameToIntegerMapper {
final class ClockCollector implements Iterable<IClock>, INameToIntegerMapper {
private HashMap<String, Integer> namesToId = new HashMap<>();
private ArrayList<IClock> clocks = new ArrayList<>();
private ArrayList<String> names = new ArrayList<>();
......@@ -21,28 +17,14 @@ final class ClockCollector implements ISpecification, Iterable<IClock>, INameToI
this.clockBuilder = clockBuilder;
}
@Override
public void addClock(String name) {
private int addClock(String name) {
Integer i = namesToId.get(name);
if (i == null) {
namesToId.put(name, clocks.size());
namesToId.put(name, i = clocks.size());
clocks.add(this.clockBuilder.buildClock(name));
names.add(name);
}
}
@Override
public void add(IDefinition definition) {
addClock(definition.getDefinedClock());
}
@Override
public void add(IRelation relation) {
// nothing to do for relations
}
@Override
public boolean isConstraintSupported(String name) {
return true;
}
return i;
}
@Override
......@@ -52,14 +34,16 @@ final class ClockCollector implements ISpecification, Iterable<IClock>, INameToI
@Override
public int getIdFromName(String name) {
Integer res = namesToId.get(name);
if (res == null) return -1;
return res;
return addClock(name); // builds the clock if does not exist
// Integer res = namesToId.get(name);
// if (res == null) return -1;
// return res;
}
IClock nameToClock(String name) {
if (getIdFromName(name) == -1) return null;
return idToClock(namesToId.get(name));
return idToClock(addClock(name)); // will build the clock if it does not exist
// if (getIdFromName(name) == -1) return null;
// return idToClock(namesToId.get(name));
}
IClock idToClock(int id) {
......@@ -70,11 +54,6 @@ final class ClockCollector implements ISpecification, Iterable<IClock>, INameToI
public String getNameFromId(int id) {
return names.get(id);
}
@Override
public boolean hasName(String name) {
return namesToId.containsKey(name);
}
@Override
public int size() {
......
......@@ -16,10 +16,10 @@ package fr.kairos.timesquare.ccsl.sat;
* @author fmallet
*/
public interface IBooleanSpecification {
// var0 Or(!vars)
// var0 Or Or(!vars)
void clause(String var0, String ...vars);
// !var0 or (And(vars))
// !var0 or (Or(vars))
void implies(String var0, String ...vars);
int id(String var);
......
......@@ -7,14 +7,7 @@ package fr.kairos.timesquare.ccsl.sat;
*/
public interface INameToIntegerMapper {
/**
*
* @param name
* @return true if the clock "name" is known
*/
boolean hasName(String name);
/**
*
* May create a name if does not exist
* @param name
* @return unique id for clock "name" or -1 if not known
*/
......
......@@ -14,7 +14,6 @@ import java.io.IOException;
import java.util.List;
import java.util.Scanner;
import fr.kairos.timesquare.ccsl.adapters.SimpleToGeneric;
import fr.kairos.timesquare.ccsl.simple.ISpecificationBuilder;
/**
......@@ -58,7 +57,6 @@ public class SATSolver implements IClockManager, IClockBuilder {
this.solverBuilder = solverBuilder;
this.collector = new ClockCollector(clockBuilder==null?this:clockBuilder);
specBuilder.build(new SimpleToGeneric(collector));
}
@Override
......
......@@ -36,7 +36,7 @@ public class SemanticBuilder implements ISimpleSpecification {
@Override
public void addClock(String name) {
// doNothing, if clock is not in a constraint
boolSpec.id(name);
}
@Override
......@@ -88,8 +88,17 @@ public class SemanticBuilder implements ISimpleSpecification {
public void binary(String def, String clock1, String clock2) {
boolSpec.id(def);
int chi = history(clock1) - history(clock2);
if (chi>=0) boolSpec.implies(clock2, def);
if (chi<=0) boolSpec.implies(clock1, def);
if (chi > 0) {
boolSpec.implies(clock1, def);
boolSpec.implies(def, clock1);
} else if (chi < 0) {
boolSpec.implies(clock2, def);
boolSpec.implies(def, clock2);
} else { // chi == 0
boolSpec.implies(clock1, def);
boolSpec.implies(clock2, def);
boolSpec.implies(def, clock1, clock2);
}
}
}.unfold(defClock, clocks);
}
......@@ -100,8 +109,17 @@ public class SemanticBuilder implements ISimpleSpecification {
@Override
public void binary(String def, String clock1, String clock2) {
int chi = history(clock1) - history(clock2);
if (chi>=0) boolSpec.implies(clock1, def);
if (chi<=0) boolSpec.implies(clock2, def);
if (chi > 0) {
boolSpec.implies(clock2, def);
boolSpec.implies(def, clock2);
} else if (chi < 0) {
boolSpec.implies(clock1, def);
boolSpec.implies(def, clock1);
} else {// chi == 0
boolSpec.implies(def, clock1);
boolSpec.implies(def, clock2);
boolSpec.clause(def, clock1, clock2);
}
}
}.unfold(defClock, clocks);
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment