Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
e29ecec
RDGNode: Método Longo
rafaelrabetti Sep 29, 2017
ee92ba2
Extração de métodos
eduqg Sep 29, 2017
485e9c1
RDGNode: Método longo
rafaelrabetti Sep 29, 2017
0edec00
RDGNode: Método Longo
rafaelrabetti Sep 29, 2017
be46f2d
extract method
danmoura17 Sep 29, 2017
b624f73
Extraindo metodo de escrita de arquivo e condicional de tipo de modelo
eduqg Sep 29, 2017
b42527a
Implementing extract method techinique
danmoura17 Sep 29, 2017
bfe142b
Merge branch 'master' of https://github.com/dastois/reana
danmoura17 Sep 29, 2017
3d0717c
Extraindo métodos para simplicar declaracoes
eduqg Sep 29, 2017
b4bbfef
RDGNode: Classe de dados e Classe inchada
rafaelrabetti Sep 29, 2017
e3779c5
Merge branch 'master' of https://github.com/dastois/reana
rafaelrabetti Sep 30, 2017
0b7768f
Adding interface to create initial inline
matmello Sep 30, 2017
7a0ccde
Adding class to avoid code duplication
matmello Sep 30, 2017
f89cf28
Introduzir variavel explicativa
eduqg Sep 30, 2017
4b8aff6
Merge branch 'master' of https://github.com/dastois/reana
matmello Sep 30, 2017
fc4bd9e
Merge branch 'master' of https://github.com/dastois/reana
eduqg Sep 30, 2017
dd72703
RDGNode: Código duplicado
rafaelrabetti Sep 30, 2017
92d3422
fixing name misspelling
matmello Sep 30, 2017
98523a4
Merge branch 'master' of https://github.com/dastois/reana
matmello Sep 30, 2017
4070537
Single return
matmello Sep 30, 2017
910b6c6
Big Method
danmoura17 Sep 30, 2017
8825d25
Merge branch 'master' of https://github.com/dastois/reana
danmoura17 Sep 30, 2017
d5f074b
Extracting method of big return
danmoura17 Sep 30, 2017
639e2ac
Long Method
danmoura17 Sep 30, 2017
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 17 additions & 8 deletions src/fdtmc/FDTMC.java
Original file line number Diff line number Diff line change
Expand Up @@ -208,9 +208,13 @@ public String toString() {
Iterator <Transition> itTransitions = transitionList.iterator();
while (itTransitions.hasNext()) {
Transition t = itTransitions.next();
msg += temp.getVariableName() + "=" + temp.getIndex() + ((temp.getLabel() != null) ? "(" + temp.getLabel() + ")" : "") +
msg += temp.getVariableName() + "=" + temp.getIndex()
+ ((temp.getLabel() != null) ? "(" + temp.getLabel() + ")" : "") +
" --- " + t.getActionName() + " / " + t.getProbability() +
" ---> " + t.getTarget().getVariableName() + "=" + t.getTarget().getIndex() + ((t.getTarget().getLabel() != null) ? "(" + t.getTarget().getLabel() + ")" : "") + "\n";
" ---> " + t.getTarget().getVariableName() + "="
+ t.getTarget().getIndex()
+ ((t.getTarget().getLabel() != null) ? "("
+ t.getTarget().getLabel() + ")" : "") + "\n";
}
}
}
Expand All @@ -231,16 +235,21 @@ public boolean equals(Object obj) {
FDTMC other = (FDTMC) obj;
LinkedList<List<Interface>> thisInterfaces = new LinkedList<List<Interface>>(interfaces.values());
LinkedList<List<Interface>> otherInterfaces = new LinkedList<List<Interface>>(other.interfaces.values());
return states.equals(other.states)
&& getInitialState().equals(other.getInitialState())
&& getSuccessState().equals(other.getSuccessState())
&& getErrorState().equals(other.getErrorState())
&& transitionSystem.equals(other.transitionSystem)
&& thisInterfaces.equals(otherInterfaces);
return compareStateAttributes(other, thisInterfaces, otherInterfaces);
}
return false;
}

private boolean compareStateAttributes(FDTMC other, LinkedList<List<Interface>> thisInterfaces,
LinkedList<List<Interface>> otherInterfaces) {
return states.equals(other.states)
&& getInitialState().equals(other.getInitialState())
&& getSuccessState().equals(other.getSuccessState())
&& getErrorState().equals(other.getErrorState())
&& transitionSystem.equals(other.transitionSystem)
&& thisInterfaces.equals(otherInterfaces);
}

@Override
public int hashCode() {
return states.hashCode() + transitionSystem.hashCode() + interfaces.hashCode();
Expand Down
52 changes: 52 additions & 0 deletions src/fdtmc/Inline.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,52 @@
package fdtmc;

public class Inline {

private Interface iface;
private FDTMC fragment;

private State initialInlined;
private State initialFragment;
private State successInlined;
private State successFragment;
private State errorInlined;
private State errorFragment;

public Inline(Interface iface, FDTMC fragment) {

this.iface = iface;
this.fragment = fragment;

this.initialInlined = iface.getInitial();
this.initialFragment = fragment.getInitialState();
this.successInlined = iface.getSuccess();
this.successFragment = fragment.getSuccessState();
this.errorInlined = iface.getError();
this.errorFragment = fragment.getErrorState();

}

public State getInitialInlined() {
return initialInlined;
}

public State getInitialFragment() {
return initialFragment;
}

public State getSuccessInlined() {
return successInlined;
}

public State getSuccessFragment() {
return successFragment;
}

public State getErrorInlined() {
return errorInlined;
}

public State getErrorFragment() {
return errorFragment;
}
}
14 changes: 9 additions & 5 deletions src/fdtmc/Interface.java
Original file line number Diff line number Diff line change
Expand Up @@ -53,15 +53,19 @@ public String getAbstractedId() {
public boolean equals(Object obj) {
if (obj != null && obj instanceof Interface) {
Interface other = (Interface) obj;
return initial.equals(other.initial)
&& success.equals(other.success)
&& error.equals(other.error)
&& successTransition.equals(other.successTransition)
&& errorTransition.equals(other.errorTransition);
return compareInterfaceAtributtes(other);
}
return false;
}

private boolean compareInterfaceAtributtes(Interface other) {
return initial.equals(other.initial)
&& success.equals(other.success)
&& error.equals(other.error)
&& successTransition.equals(other.successTransition)
&& errorTransition.equals(other.errorTransition);
}

@Override
public int hashCode() {
return initial.hashCode()
Expand Down
7 changes: 4 additions & 3 deletions src/fdtmc/State.java
Original file line number Diff line number Diff line change
Expand Up @@ -34,13 +34,14 @@ public String getLabel() {
* A state is equal to another one if they have equal indices.
* Labels are only considered when comparing FDTMCs as a whole.
*/
@Override
@Override
public boolean equals(Object obj) {
boolean isEqual = false;
if (obj != null && obj instanceof State) {
State other = (State) obj;
return this.index == other.index;
isEqual = this.index == other.index;
}
return false;
return isEqual;
}

@Override
Expand Down
62 changes: 35 additions & 27 deletions src/paramwrapper/ParamModel.java
Original file line number Diff line number Diff line change
Expand Up @@ -22,16 +22,16 @@
class ParamModel {
private String stateVariable = "s";
// TODO Deixar nome do módulo PARAM configurável.
private String moduleName = "dummyModule";
private final String moduleName = "dummyModule";
// TODO Inferir estado inicial a partir da topologia da FDTMC.
private int initialState = 0;

private Set<String> parameters;
private Map<String, Set<Integer>> labels;
private Map<Integer, Command> commands;
private final Set<String> parameters;
private final Map<String, Set<Integer>> labels;
private final Map<Integer, Command> commands;

private int stateRangeStart;
private int stateRangeEnd;
private final int stateRangeStart;
private final int stateRangeEnd;

public ParamModel(FDTMC fdtmc) {
if (fdtmc.getVariableName() != null) {
Expand All @@ -50,13 +50,13 @@ public ParamModel(FDTMC fdtmc) {
private Map<String, Set<Integer>> getLabels(FDTMC fdtmc) {
Map<String, Set<Integer>> labeledStates = new TreeMap<String, Set<Integer>>();
Collection<State> states = fdtmc.getStates();
for (State s : states) {
String label = s.getLabel();
for (State actualState : states) {
String label = actualState.getLabel();
if (label != null) {
if (!labeledStates.containsKey(label)) {
labeledStates.put(label, new TreeSet<Integer>());
}
labeledStates.get(label).add(s.getIndex());
labeledStates.get(label).add(actualState.getIndex());
}
}
return labeledStates;
Expand Down Expand Up @@ -88,9 +88,9 @@ private Set<String> getParameters(Collection<Command> commands) {
Pattern validIdentifier = Pattern.compile("[A-Za-z_][A-Za-z0-9_]*");
for (Command command : commands) {
for (String probability : command.getUpdatesProbabilities()) {
Matcher m = validIdentifier.matcher(probability);
while (m.find()) {
tmpParameters.add(m.group());
Matcher matcherToFind = validIdentifier.matcher(probability);
while (matcherToFind.find()) {
tmpParameters.add(matcherToFind.group());
}
}
}
Expand All @@ -103,14 +103,7 @@ public String toString() {
for (String parameter : parameters) {
params += "param double "+parameter+";\n";
}
String module =
"dtmc\n" +
"\n" +
params +
"\n" +
"module " + moduleName + "\n" +
" "+stateVariable+ " : ["+stateRangeStart+".."+stateRangeEnd+"] init "+initialState+";" +
"\n";
String module = moduleString(params);
for (Command command : commands.values()) {
module += " "+command.makeString(stateVariable) + "\n";
}
Expand All @@ -121,17 +114,32 @@ public String toString() {

Set<Integer> states = entry.getValue();
int count = 1;
for (Integer state : states) {
module += stateVariable+"="+state;
if (count < states.size()) {
module += " | ";
}
count++;
}
module = changeModuleState(module, states, count);
module += ";\n";
}
return module;
}

private String changeModuleState(String module, Set<Integer> states, int count) {
for (Integer state : states) {
module += stateVariable+"="+state;
if (count < states.size()) {
module += " | ";
}
count++;
}
return module;
}

private String moduleString(String params) {
return "dtmc\n" +
"\n" +
params +
"\n" +
"module " + moduleName + "\n" +
" "+stateVariable+ " : ["+stateRangeStart+".."+stateRangeEnd+"] init "+initialState+";" +
"\n";
}
}

class Command {
Expand Down
50 changes: 34 additions & 16 deletions src/paramwrapper/ParamWrapper.java
Original file line number Diff line number Diff line change
Expand Up @@ -46,38 +46,56 @@ public String getReliability(FDTMC fdtmc) {
}

private String evaluate(String model, String property) {
final String stringToBeReplaced = "\\s+";
try {
File modelFile = File.createTempFile("model", "param");
FileWriter modelWriter = new FileWriter(modelFile);
modelWriter.write(model);
modelWriter.flush();
modelWriter.close();
writeAndFlushFile(modelFile, modelWriter, model);

File propertyFile = File.createTempFile("property", "prop");
FileWriter propertyWriter = new FileWriter(propertyFile);
propertyWriter.write(property);
propertyWriter.flush();
propertyWriter.close();
writeAndFlushFile(propertyFile, propertyWriter, property);

File resultsFile = File.createTempFile("result", null);

String formula;
if (usePrism && !model.contains("param")) {
formula = invokeModelChecker(modelFile.getAbsolutePath(),
propertyFile.getAbsolutePath(),
resultsFile.getAbsolutePath());
} else {
formula = invokeParametricModelChecker(modelFile.getAbsolutePath(),
propertyFile.getAbsolutePath(),
resultsFile.getAbsolutePath());
}
return formula.trim().replaceAll("\\s+", "");
formula = invokeTypeModelChecker(model, modelFile, propertyFile, resultsFile);
return formula.trim().replaceAll(stringToBeReplaced, "");
} catch (IOException e) {
LOGGER.log(Level.SEVERE, e.toString(), e);
}
return "";
}

private String invokeTypeModelChecker(String model,
File modelFile,
File propertyFile,
File resultsFile) throws IOException {
String formula;
final boolean modelContainParam = model.contains("param");
if (usePrism && !modelContainParam) {
formula = invokeModelChecker(modelFile.getAbsolutePath(),
propertyFile.getAbsolutePath(),
resultsFile.getAbsolutePath());
} else {
formula = invokeParametricModelChecker(modelFile.getAbsolutePath(),
propertyFile.getAbsolutePath(),
resultsFile.getAbsolutePath());
}
return formula;
}

private void writeAndFlushFile(File file, FileWriter writer, String model) {
try {
writer.write(model);
writer.flush();
writer.close();
} catch (IOException e) {
LOGGER.log(Level.SEVERE, e.toString(), e);
}

}

private String invokeParametricModelChecker(String modelPath,
String propertyPath,
String resultsPath) throws IOException {
Expand Down
Loading