diff --git a/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java b/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java index c80012f09602750d7fb88b91f310300e4bac887a..58817d15a8cec36acf50ee0cb7dd5808ea346f30 100644 --- a/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java +++ b/src/main/java/avatartranslator/AvatarCompactDependencyGraph.java @@ -530,7 +530,7 @@ public class AvatarCompactDependencyGraph { if (_elt instanceof AvatarTransition) { AvatarTransition at = (AvatarTransition) _elt; - if (at.isEmpty()) { + if (at.isEmpty() && !at.isGuarded()) { if (_elt.getNext(0) != null) { return makeCompactDependencyGraphForAvatarElement(bl, _elt.getNext(0), _previousS, _elt, _states, _transitions, withID, null); @@ -777,6 +777,8 @@ public class AvatarCompactDependencyGraph { } } + AvatarSpecification oldSpec = null; + // We make the relations between blocks for (AUTState st : graph.getStates()) { if (st.getNbInTransitions() == 0) { @@ -790,7 +792,7 @@ public class AvatarCompactDependencyGraph { AvatarBlock newBlock = newAvspec.getBlockWithName(ab.getName()); if (newBlock != null) { // We add relations for which the two related blocks have been defined - AvatarSpecification oldSpec = asmo.getAvatarSpecification(); + oldSpec = asmo.getAvatarSpecification(); if (oldSpec != null) { for (AvatarRelation ar: oldSpec.getRelations()) { boolean b1 = ar.getBlock1().getName().compareTo(newBlock.getName()) == 0; @@ -826,6 +828,13 @@ public class AvatarCompactDependencyGraph { } } + // We clone the datatypes + if (!oldSpec.getDataTypes().isEmpty()) { + for (AvatarDataType adt : oldSpec.getDataTypes()) { + newAvspec.addDataType(adt.advancedClone()); + } + } + // We make the state machines for (AUTState st : graph.getStates()) { diff --git a/src/main/java/cli/Action.java b/src/main/java/cli/Action.java index 275cda3c7c0994393184df39e2c602aa5f05bc5d..e460bea6639a059c5b0d2613d2c63a6c14e36972 100644 --- a/src/main/java/cli/Action.java +++ b/src/main/java/cli/Action.java @@ -1658,7 +1658,10 @@ public class Action extends Command implements ProVerifOutputListener { interpreter.mgui.addRG(rg); // 3. Generate new Avatar spec + acdgReduced.setGraph(result); as = acdgReduced.makeAvatarSpecification(); + interpreter.mgui.drawAvatarSpecification(as, true); + TraceManager.addUser(as.toString()); return null; }