Commit 66476484 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean

Updated

parent bc642d3e
Pipeline #2523 skipped
......@@ -2,13 +2,11 @@ package sut.tcp;
import invlang.types.FlagSet;
public interface ConcretizationInterface {
public interface ConcretizationInterface{
public String processIncomingRequest(FlagSet flags, Integer concSeq,
Integer concAck, int payloadLength);
public String processOutgoingResponse(FlagSet flags, String absSeq,
String absAck, int payloadLength);
public String processIncomingRequest(FlagSet flags, Integer concSeq,
Integer concAck, int payloadLength);
public void reset();
}
......@@ -13,11 +13,11 @@ import util.OutputAction;
public class ConcretizingMapper implements ConcretizationInterface{
private InvLangHandler handler;
private RandomConcretizer concretizer;
private ResponseConcretizer concretizer;
public ConcretizingMapper(InvLangHandler handler) {
this.handler = handler;
this.concretizer = new RandomConcretizer(handler);
this.concretizer = new InvlangConcretizer(handler);
}
......
package sut.tcp;
import exceptions.BugException;
import invlang.mapperReader.InvLangHandler;
import invlang.types.FlagSet;
import sut.tcp.InvlangMapper.Inputs;
import sut.tcp.InvlangMapper.Mappings;
import sut.tcp.InvlangMapper.Outputs;
import util.OutputAction;
public class InvlangConcretizer implements ResponseConcretizer{
private InvLangHandler handler;
private RandomResponseConcretizer fallback;
public InvlangConcretizer(InvLangHandler handler) {
this.handler = handler;
this.fallback = new RandomResponseConcretizer(handler);
}
@Override
public OutputAction concretizeResponse(FlagSet flags, String absSeq, String absAck, int payloadLength) {
handler.setEnum(Inputs.ABS_SEQ, "abssut", absSeq);
handler.setEnum(Inputs.ABS_ACK, "abslearner", absAck);
// handler.setInt(Outputs.ABS_DATA, payloadLength);
handler.executeInverted(Mappings.INCOMING_RESPONSE);
if (handler.hasResult()) {
int concSeq = handler.getIntResult(Inputs.CONC_SEQ);
int concAck = handler.getIntResult(Inputs.CONC_ACK);
System.out.println(concSeq + " " + concAck);
OutputAction output = new OutputAction(flags.toString(), new Integer [] {concSeq, concAck, payloadLength});
return output;
} else {
OutputAction output = this.fallback.concretizeResponse(flags, absSeq, absAck, payloadLength);
if (output != null) {
throw new BugException("This one works");
}
throw new BugException("Couldn't concretize " + handler.getState());
}
}
}
......@@ -22,18 +22,22 @@ import invlang.types.FlagSet;
*
* This is used as an alternative to executeInverted called on the handler.
*/
public class RandomConcretizer {
public class RandomResponseConcretizer implements ResponseConcretizer{
private InvLangHandler handler;
public RandomConcretizer(InvLangHandler handler) {
public RandomResponseConcretizer(InvLangHandler handler) {
this.handler = handler;
}
@Override
public OutputAction concretizeResponse(FlagSet flags, String absSeq,
String absAck, int payloadLength) {
Configuration freshConfiguration = generateFreshConfiguration();
List<Integer> pointsOfInterest = getPointsOfInterest();
List<Configuration> configurations = generateConfigurations(freshConfiguration, pointsOfInterest);
Configuration foundConfig = getFirstConfigurationMatchingAbstractions(configurations, flags, absSeq, absAck, payloadLength);
List<Integer> pointsOfInterest = getPointsOfInterest(15);
//List<Configuration> configurations = generateConfigurations(freshConfiguration, pointsOfInterest);
Configuration foundConfig = getFirstConfigurationMatchingAbstractions(freshConfiguration, pointsOfInterest,
flags, absSeq, absAck, payloadLength);
if (foundConfig == null) {
throw new BugException("Cannot concretize the output " + flags + "(" + absSeq + "," + absAck + "," + payloadLength + ")"
......@@ -71,12 +75,31 @@ public class RandomConcretizer {
}
private Configuration getFirstConfigurationMatchingAbstractions(
List<Configuration> testConfigurations, FlagSet flags, String absSeq, String absAck, int payloadLength) {
for (Configuration config : testConfigurations) {
if (checkIfValidConcretization(flags, absSeq, config.seqNum, absAck, config.ackNum, payloadLength)) {
return config;
Configuration fresh, List<Integer> pointsOfInterest, FlagSet flags, String absSeq, String absAck, int payloadLength) {
if (checkIfValidConcretization(flags, absSeq, fresh.seqNum, absAck, fresh.ackNum, payloadLength) ){
return fresh;
} else {
for (Integer possibleAck : pointsOfInterest) {
if (checkIfValidConcretization(flags, absSeq, fresh.seqNum, absAck, possibleAck, payloadLength) ){
return new Configuration(fresh.seqNum, possibleAck);
}
}
for (Integer possibleSeq : pointsOfInterest) {
if (checkIfValidConcretization(flags, absSeq, possibleSeq, absAck, fresh.ackNum, payloadLength) ){
return new Configuration(possibleSeq, fresh.ackNum);
}
}
for (Integer possibleSeq : pointsOfInterest) {
for (Integer possibleAck : pointsOfInterest) {
if (checkIfValidConcretization(flags, absSeq, possibleSeq, absAck, possibleAck, payloadLength) ){
return new Configuration(possibleSeq, possibleAck);
}
}
}
}
return null;
}
......@@ -84,6 +107,8 @@ public class RandomConcretizer {
* Generates an ordered list of sequence and acknowledgement number configurations from a freshSeq, freshAck and pointsOfInterest.
* Configurations using fresh values appear before those only made from points of interest. In a later version, these fresh
* values will be included in the points of interest, and not treated differently.
*
* The advantage of storing to a list is that you can shuffle it (for bettter testing).
*/
private List<Configuration> generateConfigurations(Configuration freshConfiguration, List<Integer> pointsOfInterest) {
List<Configuration> seqAckConfigurations = new LinkedList<>();
......@@ -115,14 +140,14 @@ public class RandomConcretizer {
}
}
private List<Integer> getPointsOfInterest() {
private List<Integer> getPointsOfInterest(int numberOfIncrements) {
List<Integer> valuesOfInterest = new ArrayList<Integer>();
for (Entry<String, Object> entry : this.handler.getState().entrySet()) {
if (entry.getValue() instanceof Integer) {
int value = (Integer) entry.getValue();
if (value != InvlangMapper.NOT_SET && !valuesOfInterest.contains(value)) {
for (int i=0; i < 20; i ++) {
for (int i=0; i < numberOfIncrements; i ++) {
if (!valuesOfInterest.contains(value+i)) {
valuesOfInterest.add(value+i);
}
......@@ -178,6 +203,7 @@ public class RandomConcretizer {
// handler.setInt(Outputs.CONC_DATA, payloadLength);
// handler.execute(Mappings.OUTGOING_REQUEST);
}
// private List<Long> getPointsOfInterest() {
......
package sut.tcp;
import invlang.types.FlagSet;
import util.OutputAction;
public interface ResponseConcretizer {
public OutputAction concretizeResponse(FlagSet flags, String absSeq,
String absAck, int payloadLength);
}
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