diff --git a/src/fdtmc/FDTMC.java b/src/fdtmc/FDTMC.java index ef21282..6ed7349 100644 --- a/src/fdtmc/FDTMC.java +++ b/src/fdtmc/FDTMC.java @@ -208,9 +208,13 @@ public String toString() { Iterator 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"; } } } @@ -231,16 +235,21 @@ public boolean equals(Object obj) { FDTMC other = (FDTMC) obj; LinkedList> thisInterfaces = new LinkedList>(interfaces.values()); LinkedList> otherInterfaces = new LinkedList>(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> thisInterfaces, + LinkedList> 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(); diff --git a/src/fdtmc/Inline.java b/src/fdtmc/Inline.java new file mode 100644 index 0000000..20f2e6e --- /dev/null +++ b/src/fdtmc/Inline.java @@ -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; + } +} diff --git a/src/fdtmc/Interface.java b/src/fdtmc/Interface.java index f6cd969..0582b49 100644 --- a/src/fdtmc/Interface.java +++ b/src/fdtmc/Interface.java @@ -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() diff --git a/src/fdtmc/State.java b/src/fdtmc/State.java index 3d0b1f9..b72d708 100644 --- a/src/fdtmc/State.java +++ b/src/fdtmc/State.java @@ -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 diff --git a/src/paramwrapper/ParamModel.java b/src/paramwrapper/ParamModel.java index ddd77e4..0ef357e 100644 --- a/src/paramwrapper/ParamModel.java +++ b/src/paramwrapper/ParamModel.java @@ -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 parameters; - private Map> labels; - private Map commands; + private final Set parameters; + private final Map> labels; + private final Map commands; - private int stateRangeStart; - private int stateRangeEnd; + private final int stateRangeStart; + private final int stateRangeEnd; public ParamModel(FDTMC fdtmc) { if (fdtmc.getVariableName() != null) { @@ -50,13 +50,13 @@ public ParamModel(FDTMC fdtmc) { private Map> getLabels(FDTMC fdtmc) { Map> labeledStates = new TreeMap>(); Collection 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()); } - labeledStates.get(label).add(s.getIndex()); + labeledStates.get(label).add(actualState.getIndex()); } } return labeledStates; @@ -88,9 +88,9 @@ private Set getParameters(Collection 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()); } } } @@ -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"; } @@ -121,17 +114,32 @@ public String toString() { Set 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 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 { diff --git a/src/paramwrapper/ParamWrapper.java b/src/paramwrapper/ParamWrapper.java index 1b34cb8..a51824d 100644 --- a/src/paramwrapper/ParamWrapper.java +++ b/src/paramwrapper/ParamWrapper.java @@ -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 { diff --git a/src/tool/RDGNode.java b/src/tool/RDGNode.java index 180097c..81beca9 100644 --- a/src/tool/RDGNode.java +++ b/src/tool/RDGNode.java @@ -1,5 +1,4 @@ package tool; -import java.util.Collection; import java.util.HashMap; import java.util.HashSet; import java.util.LinkedList; @@ -17,21 +16,7 @@ public class RDGNode { private static int lastNodeIndex = 0; - // Node identifier - private String id; - //This attribute is used to store the FDTMC for the RDG node. - private FDTMC fdtmc; - /** - * The node must have an associated presence condition, which is - * a boolean expression over features. - */ - private String presenceCondition; - // Nodes on which this one depends - private Collection dependencies; - /** - * Height of the RDGNode. - */ - private int height; + private RDGNodeData data = new RDGNodeData(); /** @@ -45,45 +30,20 @@ public class RDGNode { * this node. */ public RDGNode(String id, String presenceCondition, FDTMC fdtmc) { - this.id = id; - this.presenceCondition = presenceCondition; - this.fdtmc = fdtmc; - this.dependencies = new HashSet(); - this.height = 0; + this.data.setId(id); + this.data.setPresenceCondition(presenceCondition); + this.data.setFdtmc(fdtmc); + this.data.setDependencies(new HashSet()); + this.data.setHeight(0); rdgNodes.put(id, this); nodesInCreationOrder.add(this); } - public FDTMC getFDTMC() { - return this.fdtmc; - } - - public void addDependency(RDGNode child) { - this.dependencies.add(child); - height = Math.max(height, child.height + 1); - } - - public Collection getDependencies() { - return dependencies; - } - - public String getPresenceCondition() { - return presenceCondition; - } - - public String getId() { - return id; - } - - /** - * Height of the RDGNode. This metric is defined in the same way as - * the height of a tree node, i.e., the maximum number of nodes in a path - * from this one to a leaf (node with no dependencies). - */ - public int getHeight() { - return height; - } + public void addDependency(RDGNode child) { + this.data.dependencies.add(child); + data.height = Math.max(data.height, child.data.height + 1); + } public static RDGNode getById(String id) { return rdgNodes.get(id); @@ -100,23 +60,39 @@ public static String getNextId() { */ @Override public boolean equals(Object obj) { - if (obj != null && obj instanceof RDGNode) { + if (notNullAndSameInstance(obj)) { RDGNode other = (RDGNode) obj; - return this.getPresenceCondition().equals(other.getPresenceCondition()) - && this.getFDTMC().equals(other.getFDTMC()) - && this.getDependencies().equals(other.getDependencies()); + return hasSamePresenceCondition(other) + && hasSameFDTMC(other) + && hasSameDependencies(other); } return false; } + private boolean notNullAndSameInstance(Object obj) { + return obj != null && obj instanceof RDGNode; + } + + private boolean hasSameDependencies(RDGNode other) { + return this.data.getDependencies().equals(other.data.getDependencies()); + } + + private boolean hasSameFDTMC(RDGNode other) { + return this.data.getFdtmc().equals(other.data.getFdtmc()); + } + + private boolean hasSamePresenceCondition(RDGNode other) { + return this.data.getPresenceCondition().equals(other.data.getPresenceCondition()); + } + @Override public int hashCode() { - return id.hashCode() + presenceCondition.hashCode() + fdtmc.hashCode() + dependencies.hashCode(); + return data.id.hashCode() + data.presenceCondition.hashCode() + data.fdtmc.hashCode() + data.dependencies.hashCode(); } @Override public String toString() { - return getId() + " (" + getPresenceCondition() + ")"; + return data.getId() + " (" + data.getPresenceCondition() + ")"; } /** @@ -143,21 +119,30 @@ public List getDependenciesTransitiveClosure() throws CyclicRdgExceptio * @throws CyclicRdgException */ private void topoSortVisit(RDGNode node, Map marks, List sorted) throws CyclicRdgException { - if (marks.containsKey(node) && marks.get(node) == false) { + if (containsKeyAndNotHaveNode(node, marks)) { // Visiting temporarily marked node -- this means a cyclic dependency! throw new CyclicRdgException(); - } else if (!marks.containsKey(node)) { + } else if (doesNotContainKey(node, marks)) { // Mark node temporarily (cycle detection) - marks.put(node, false); - for (RDGNode child: node.getDependencies()) { - topoSortVisit(child, marks, sorted); - } + addNodeToMap(node, marks, false); + getDependenciesForEachChild(node, marks, sorted); // Mark node permanently (finished sorting branch) - marks.put(node, true); + addNodeToMap(node, marks, true); sorted.add(node); } } + private static boolean doesNotContainKey(RDGNode node, Map marks) { + return !marks.containsKey(node); + } + + private void getDependenciesForEachChild(RDGNode node, Map marks, List sorted) + throws CyclicRdgException { + for (RDGNode child: node.data.getDependencies()) { + topoSortVisit(child, marks, sorted); + } + } + /** * Computes the number of paths from source nodes to every known node. * @return A map associating an RDGNode to the corresponding number @@ -177,24 +162,21 @@ public Map getNumberOfPaths() throws CyclicRdgException { // TODO Parameterize topological sort of RDG. private static Map numPathsVisit(RDGNode node, Map marks, Map> cache) throws CyclicRdgException { - if (marks.containsKey(node) && marks.get(node) == false) { + if (containsKeyAndNotHaveNode(node, marks)) { // Visiting temporarily marked node -- this means a cyclic dependency! throw new CyclicRdgException(); - } else if (!marks.containsKey(node)) { + } else if (doesNotContainKey(node, marks)) { // Mark node temporarily (cycle detection) - marks.put(node, false); + addNodeToMap(node, marks, false); Map numberOfPaths = new HashMap(); // A node always has a path to itself. numberOfPaths.put(node, 1); // The number of paths from a node X to a node Y is equal to the // sum of the numbers of paths from each of its descendants to Y. - for (RDGNode child: node.getDependencies()) { - Map tmpNumberOfPaths = numPathsVisit(child, marks, cache); - numberOfPaths = sumPaths(numberOfPaths, tmpNumberOfPaths); - } + numberOfPaths = getDependenciesForEachChild(node, marks, cache, numberOfPaths); // Mark node permanently (finished sorting branch) - marks.put(node, true); + addNodeToMap(node, marks, true); cache.put(node, numberOfPaths); return numberOfPaths; } @@ -202,6 +184,23 @@ private static Map numPathsVisit(RDGNode node, Map marks, boolean bool) { + marks.put(node, bool); + } + + private static boolean containsKeyAndNotHaveNode(RDGNode node, Map marks) { + return marks.containsKey(node) && marks.get(node) == false; + } + + private static Map getDependenciesForEachChild(RDGNode node, Map marks, + Map> cache, Map numberOfPaths) throws CyclicRdgException { + for (RDGNode child: node.data.getDependencies()) { + Map tmpNumberOfPaths = numPathsVisit(child, marks, cache); + numberOfPaths = sumPaths(numberOfPaths, tmpNumberOfPaths); + } + return numberOfPaths; + } + /** * Sums two paths-counting maps * @param pathsCountA @@ -210,7 +209,13 @@ private static Map numPathsVisit(RDGNode node, Map sumPaths(Map pathsCountA, Map pathsCountB) { Map numberOfPaths = new HashMap(pathsCountA); - for (Map.Entry entry: pathsCountB.entrySet()) { + pathsCountBEntrySetForEachEntry(pathsCountB, numberOfPaths); + return numberOfPaths; + } + + private static void pathsCountBEntrySetForEachEntry(Map pathsCountB, + Map numberOfPaths) { + for (Map.Entry entry: pathsCountB.entrySet()) { RDGNode node = entry.getKey(); Integer count = entry.getValue(); if (numberOfPaths.containsKey(node)) { @@ -218,8 +223,7 @@ private static Map sumPaths(Map pathsCountA, } numberOfPaths.put(node, count); } - return numberOfPaths; - } + } /** * Returns the first RDG node (in crescent order of creation time) which is similar diff --git a/src/tool/RDGNodeData.java b/src/tool/RDGNodeData.java new file mode 100644 index 0000000..7673665 --- /dev/null +++ b/src/tool/RDGNodeData.java @@ -0,0 +1,63 @@ +package tool; + +import java.util.Collection; + +import fdtmc.FDTMC; + +public class RDGNodeData { + public String id; + public FDTMC fdtmc; + /** + * The node must have an associated presence condition, which is + * a boolean expression over features. + */ + public String presenceCondition; + public Collection dependencies; + /** + * Height of the RDGNode. + */ + public int height; + + public String getId() { + return id; + } + + public void setId(String id) { + this.id = id; + } + + public FDTMC getFdtmc() { + return fdtmc; + } + + public void setFdtmc(FDTMC fdtmc) { + this.fdtmc = fdtmc; + } + + public String getPresenceCondition() { + return presenceCondition; + } + + public void setPresenceCondition(String presenceCondition) { + this.presenceCondition = presenceCondition; + } + + public Collection getDependencies() { + return dependencies; + } + + public void setDependencies(Collection dependencies) { + this.dependencies = dependencies; + } + + public int getHeight() { + return height; + } + + public void setHeight(int height) { + this.height = height; + } + + public RDGNodeData() { + } +} \ No newline at end of file diff --git a/test/fdtmc/FDTMCTest.java b/test/fdtmc/FDTMCTest.java index 79da213..f649639 100644 --- a/test/fdtmc/FDTMCTest.java +++ b/test/fdtmc/FDTMCTest.java @@ -54,28 +54,40 @@ public void testCreateLotsOfStates() { s4 = fdtmc1.createState(); s5 = fdtmc1.createState(); - Assert.assertNotNull(s0); - Assert.assertNotNull(s1); - Assert.assertNotNull(s2); - Assert.assertNotNull(s3); - Assert.assertNotNull(s4); - Assert.assertNotNull(s5); + assertStatesNotNull(s0, s1, s2, s3, s4, s5); - Assert.assertTrue(fdtmc1.getStates().contains(s0)); - Assert.assertTrue(fdtmc1.getStates().contains(s1)); - Assert.assertTrue(fdtmc1.getStates().contains(s2)); - Assert.assertTrue(fdtmc1.getStates().contains(s3)); - Assert.assertTrue(fdtmc1.getStates().contains(s4)); - Assert.assertTrue(fdtmc1.getStates().contains(s5)); + assertTrueTheStates(s0, s1, s2, s3, s4, s5); + + assertEqualsTheStates(s0, s1, s2, s3, s4, s5); + + Assert.assertEquals(s0, fdtmc1.getInitialState()); + } + private void assertEqualsTheStates(State s0, State s1, State s2, State s3, State s4, State s5) { Assert.assertEquals(0, s0.getIndex()); Assert.assertEquals(1, s1.getIndex()); Assert.assertEquals(2, s2.getIndex()); Assert.assertEquals(3, s3.getIndex()); Assert.assertEquals(4, s4.getIndex()); Assert.assertEquals(5, s5.getIndex()); + } - Assert.assertEquals(s0, fdtmc1.getInitialState()); + private void assertTrueTheStates(State s0, State s1, State s2, State s3, State s4, State s5) { + Assert.assertTrue(fdtmc1.getStates().contains(s0)); + Assert.assertTrue(fdtmc1.getStates().contains(s1)); + Assert.assertTrue(fdtmc1.getStates().contains(s2)); + Assert.assertTrue(fdtmc1.getStates().contains(s3)); + Assert.assertTrue(fdtmc1.getStates().contains(s4)); + Assert.assertTrue(fdtmc1.getStates().contains(s5)); + } + + private void assertStatesNotNull(State s0, State s1, State s2, State s3, State s4, State s5) { + Assert.assertNotNull(s0); + Assert.assertNotNull(s1); + Assert.assertNotNull(s2); + Assert.assertNotNull(s3); + Assert.assertNotNull(s4); + Assert.assertNotNull(s5); } diff --git a/test/paramwrapper/FDTMCToParamTest.java b/test/paramwrapper/FDTMCToParamTest.java index f3ddcaa..5f2af55 100644 --- a/test/paramwrapper/FDTMCToParamTest.java +++ b/test/paramwrapper/FDTMCToParamTest.java @@ -23,29 +23,37 @@ public void setUp() throws Exception { public void testSingletonFDTMC() { FDTMC singletonFDTMC = new FDTMC(); singletonFDTMC.setVariableName("s"); - State s = singletonFDTMC.createState(); - singletonFDTMC.createTransition(s, s, null, "1"); + State stateSingleton = singletonFDTMC.createState(); + singletonFDTMC.createTransition(stateSingleton, stateSingleton, null, "1"); - String expectedModule = - "dtmc\n" + String expectedModule = stringExpectedModule(); + + assertEquals(expectedModule, paramWrapper.fdtmcToParam(singletonFDTMC)); + } + + private String stringExpectedModule() { + return "dtmc\n" + "\n\n" + "module dummyModule\n" + " s : [0..1] init 0;\n" + " [] s=0 -> (1) : (s'=0);\n" + "endmodule\n\n"; - - assertEquals(expectedModule, paramWrapper.fdtmcToParam(singletonFDTMC)); } @Test public void testSingletonFDTMCWithLabel() { FDTMC singletonFDTMC = new FDTMC(); singletonFDTMC.setVariableName("s"); - State s = singletonFDTMC.createState("success"); - singletonFDTMC.createTransition(s, s, null, "1"); + State stateSingleton = singletonFDTMC.createState("success"); + singletonFDTMC.createTransition(stateSingleton, stateSingleton, null, "1"); - String expectedModule = - "dtmc\n" + String expectedModule = stringExpectedModuleWithLabel(); + + assertEquals(expectedModule, paramWrapper.fdtmcToParam(singletonFDTMC)); + } + + private String stringExpectedModuleWithLabel() { + return "dtmc\n" + "\n\n" + "module dummyModule\n" + " s : [0..1] init 0;\n" @@ -53,8 +61,6 @@ public void testSingletonFDTMCWithLabel() { + "endmodule\n" + "\n" + "label \"success\" = s=0;\n"; - - assertEquals(expectedModule, paramWrapper.fdtmcToParam(singletonFDTMC)); } @Test @@ -67,8 +73,13 @@ public void testSimpleFDTMCWithParameters() { fdtmc.createTransition(s0, s1, null, "1-rLoop"); fdtmc.createTransition(s1, s1, null, "1"); - String expectedModule = - "dtmc\n" + String expectedModule = stringExpectedModuleWithParams(); + + assertEquals(expectedModule, paramWrapper.fdtmcToParam(fdtmc)); + } + + private String stringExpectedModuleWithParams() { + return "dtmc\n" + "\n" + "param double rLoop;\n" + "\n" @@ -77,11 +88,8 @@ public void testSimpleFDTMCWithParameters() { + " [] s=0 -> (rLoop) : (s'=0) + (1-rLoop) : (s'=1);\n" + " [] s=1 -> (1) : (s'=1);\n" + "endmodule\n\n"; - - assertEquals(expectedModule, paramWrapper.fdtmcToParam(fdtmc)); } - @Test public void testSimpleFDTMCWithParametersAndLabels() { FDTMC fdtmc = new FDTMC(); @@ -97,8 +105,13 @@ public void testSimpleFDTMCWithParametersAndLabels() { fdtmc.createTransition(s2, s2, null, "1"); fdtmc.createTransition(s3, s3, null, "1"); - String expectedModule = - "dtmc\n" + String expectedModule = stringExpectedModuleWithParamsAndLabels(); + + assertEquals(expectedModule, paramWrapper.fdtmcToParam(fdtmc)); + } + + private String stringExpectedModuleWithParamsAndLabels() { + return "dtmc\n" + "\n" + "param double rFail;\n" + "param double rLoop;\n" @@ -113,9 +126,5 @@ public void testSimpleFDTMCWithParametersAndLabels() { + "\n" + "label \"error\" = s=3;\n" + "label \"success\" = s=1 | s=2;\n"; - - assertEquals(expectedModule, paramWrapper.fdtmcToParam(fdtmc)); } - - // Many states with one label }