diff --git a/README.md b/README.md index 7718b8a..404078e 100644 --- a/README.md +++ b/README.md @@ -24,15 +24,17 @@ This guide explains usage of ALDB, compatibility requirements for Alloy models, ## Getting Started 1. Download the latest JAR from the [releases](https://github.com/WatForm/aldb/releases) or clone this repo and build ALDB following the instructions in the [contributing guildlines](./CONTRIBUTING.md). Note that the master branch points to the latest, unstable, development version of ALDB. + +2. Graphviz needs to be installed locally for visualization components. Graphviz can be downloaded [here](https://graphviz.org/download/). To check if graphviz has been successfully installed, entered `dot -v` in the command line. -2. Run ALDB from the command line: +3. Run ALDB from the command line: ```sh $ java -jar dist/aldb.jar ``` ## Model and Configuration Format -ALDB supports transition systems modelled in a certain style in Alloy. As such, there are certain signatures and predicates that are expected to exist, whose names can be stored in a custom configuration. +ALDB supports transition systems modelled in a certain style in Alloy. As such, there are certain signatures and predicates that are expected to exist, whose names can be stored in a custom configuration. ALDB supports both models in .als format and in .dsh format. To load .dsh files, enter d or dash when prompted upon launching aldb.jar. The configuration must be defined in YAML. It can be specified within a comment block in the model file (to be applied for that model only), or set via passing a separate YAML file to the `set conf` command. When using the `set conf` command, the configuration will last for the entire ALDB session. @@ -68,7 +70,7 @@ The Alloy code that conforms to the above configuration – with the configurati sig State { … } pred init[s: State] { … } -pred next[s, sprime: State] { … } +pred next[s, s’: State] { … } ``` Refer to the worked example in this guide for a sample of a concrete Alloy model that is supported by ALDB. @@ -95,6 +97,10 @@ Command | Description [step](#step) | Perform a state transition of n steps [trace](#trace) | Load a saved Alloy XML instance [until](#until) | Run until constraints are met +[show](#show) | Print out the information of a specified state +[goto](#goto) | Go to a specified state +[force](#force) | Force a transition to be taken in a specified number of steps (Dash-specific) + ### Detailed Descriptions @@ -208,6 +214,15 @@ Specify the `limit` in order to constrain the search space. In other words, ALDB ![image](https://user-images.githubusercontent.com/13455356/77835884-9a067880-7127-11ea-8808-16b692ee3ebe.png) +#### goto +The `goto [state name]` command will take steps to go to the specified state from the initial state. + +#### show +The `show [state name]` command will print out information of the specified state. + +#### force +The `force [transition name] [max steps]` command will force a transition to be taken in a specified number of steps (Dash-specific). + ## Usage Example This section will walk through solving the classic River Crossing Problem (RCP) via specification with Alloy and ALDB. @@ -236,19 +251,19 @@ pred init [s: State] { } /* At most one item to move from ‘from’ to ‘to’. */ -pred crossRiver [from, fromprime, to, toprime: set Object] { +pred crossRiver [from, from’, to, to’: set Object] { one x: from | { - fromprime = from - x - Farmer - fromprime.eats - toprime = to + x + Farmer + from’ = from - x - Farmer - from’.eats + to’ = to + x + Farmer } } /* Transition to the next state. */ -pred next [s, sprime: State] { +pred next [s, s’: State] { Farmer in s.near => - crossRiver [s.near, sprime.near, s.far, sprime.far] + crossRiver [s.near, s’.near, s.far, s’.far] else - crossRiver [s.far, sprime.far, s.near, sprime.near] + crossRiver [s.far, s’.far, s.near, s’.near] } ``` [http://alloytools.org/tutorials/online/frame-RC-1.html](http://alloytools.org/tutorials/online/frame-RC-1.html) diff --git a/lib/json-20230227.jar b/lib/json-20230227.jar new file mode 100644 index 0000000..abdb16b Binary files /dev/null and b/lib/json-20230227.jar differ diff --git a/lib/org.alloytools.alloy.dist.jar b/lib/org.alloytools.alloy.dist.jar index 8f5dccf..625e4fa 100644 Binary files a/lib/org.alloytools.alloy.dist.jar and b/lib/org.alloytools.alloy.dist.jar differ diff --git a/src/alloy/AlloyUtils.java b/src/alloy/AlloyUtils.java index 2176b0e..9545001 100644 --- a/src/alloy/AlloyUtils.java +++ b/src/alloy/AlloyUtils.java @@ -89,7 +89,10 @@ public static String annotatedTransitionSystemStep(String model, ParsingConf par public static String annotatedTransitionSystemUntil(String model, ParsingConf parsingConf, int steps) { return annotatedTransitionSystem(model, parsingConf, steps, "break[aldb_order/last]"); } - + + public static String annotatedTransitionSystemForced(String model, ParsingConf parsingConf, int steps) { + return annotatedTransitionSystem(model, parsingConf, steps, "transitionForced"); + } /** * getBreakPredicate creates a predicate containing all breakpoints entered * by the user. @@ -98,13 +101,13 @@ public static String annotatedTransitionSystemUntil(String model, ParsingConf pa */ public static String getBreakPredicate(List rawConstraints, SigData sigData) { List constraints = new ArrayList(); + for (String rawConstraint : rawConstraints) { constraints.add(String.format("(%s)", getConstraint(rawConstraint, sigData.getFields()))); } String constraintsString = String.join(String.format(" %s ", AlloyConstants.OR), constraints); String predicateBody = String.format("\t%s\n", constraintsString); - return makeStatePredicate( AlloyConstants.BREAK_PREDICATE_NAME, sigData.getLabel(), @@ -174,13 +177,12 @@ private static String getConstraint(String rawConstraint, Set fields) { if (rawConstraint.trim().isEmpty()) { return AlloyConstants.ALWAYS_TRUE; } - StringBuilder constraint = new StringBuilder(); StringBuilder buffer = new StringBuilder(); for (int i = 0; i < rawConstraint.length(); i++) { Character c = rawConstraint.charAt(i); - if (!Character.isLetterOrDigit(c)) { + if (!Character.isLetterOrDigit(c) && !c.equals('_')) { String field = buffer.toString(); if (fields.contains(field)) { String stateField = String.format("s.%s", field); @@ -204,10 +206,27 @@ private static String getConstraint(String rawConstraint, Set fields) { constraint.append(stateField); } } - + return constraint.toString(); } + + public static String getTransitionPredicate(String rawConstraint) { + StringBuilder constraint = new StringBuilder(); + + // Start building the predicate string + constraint.append("pred transitionForced {\n") + .append(" some s: DshSnapshot, sn: DshSnapshot | sn.(s.") + .append(rawConstraint).append(")\n") + .append("}"); + + return constraint.toString(); + } + + + + + /** * annotatedTransitionSystem generates Alloy code based on the following rules: * 1. Use ordering module. diff --git a/src/alloy/ParsingConf.java b/src/alloy/ParsingConf.java index 987a51e..f911537 100644 --- a/src/alloy/ParsingConf.java +++ b/src/alloy/ParsingConf.java @@ -7,6 +7,8 @@ import java.util.HashMap; import java.util.Map; + +// do comments for this public class ParsingConf { private static final String STATE_SIG_NAME_DEFAULT = "State"; private static final String INIT_PREDICATE_NAME_DEFAULT = "init"; diff --git a/src/alloy/readme.md b/src/alloy/readme.md new file mode 100644 index 0000000..916fb97 --- /dev/null +++ b/src/alloy/readme.md @@ -0,0 +1,23 @@ +# Alloy Package README + +## Overview + +This package provides a collection of classes and utilities designed to work with Alloy, a language for modeling and analyzing complex systems. The package includes constants, interfaces, and utility functions that streamline working with Alloy models, particularly in the context of generating and manipulating `.als` files and parsing configuration files. + +## Contents + +### 1. `AlloyConstants.java` +- **Purpose:** + - This class contains a set of constants that are commonly used when working with Alloy. These constants may include keywords, file paths, and other frequently used values that are essential for Alloy-based operations. + +### 2. `AlloyInterface.java` +- **Purpose:** + - This interface defines functions for interacting with Alloy models, specifically for obtaining Alloy signatures (`sigs`) and Alloy A4 solutions. The functions provided in this interface facilitate the extraction and manipulation of these elements from Alloy models. + +### 3. `AlloyUtils.java` +- **Purpose:** + - This utility class contains helper functions for formatting strings, particularly constraints, that need to be appended to `.als` files. The functions in this class assist in ensuring that constraints are correctly formatted and integrated into Alloy models. + +### 4. `ParsingConf.java` +- **Purpose:** + - This class is responsible for parsing `.yaml` configuration files. It provides functions for extracting important elements such as state names, transition names, and event names from these files, which can then be used in the context of Alloy modeling. diff --git a/src/commands/AliasCommand.java b/src/commands/AliasCommand.java index 8fdf85e..fadb366 100644 --- a/src/commands/AliasCommand.java +++ b/src/commands/AliasCommand.java @@ -1,6 +1,7 @@ package commands; import simulation.AliasManager; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.util.Arrays; @@ -32,6 +33,9 @@ public String[] getShorthand() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (input.length == 1) { System.out.println(CommandConstants.ALIAS_HELP); return; diff --git a/src/commands/AltCommand.java b/src/commands/AltCommand.java index c84a9f3..a6a068a 100644 --- a/src/commands/AltCommand.java +++ b/src/commands/AltCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class AltCommand extends Command { @@ -22,6 +23,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/BreakCommand.java b/src/commands/BreakCommand.java index 931a624..a63bfab 100644 --- a/src/commands/BreakCommand.java +++ b/src/commands/BreakCommand.java @@ -2,6 +2,7 @@ import simulation.AliasManager; import simulation.ConstraintManager; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.util.Arrays; @@ -31,6 +32,9 @@ public String[] getShorthand() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (input.length == 1) { System.out.println(CommandConstants.BREAK_HELP); return; @@ -74,7 +78,6 @@ public void execute(String[] input, SimulationManager simulationManager) { if (am.isAlias(constraint)) { constraint = am.getFormula(constraint); } - if (simulationManager.validateConstraint(constraint)) { cm.addConstraint(constraint); } else { diff --git a/src/commands/CommandConstants.java b/src/commands/CommandConstants.java index cf9ac34..1ea160a 100644 --- a/src/commands/CommandConstants.java +++ b/src/commands/CommandConstants.java @@ -3,6 +3,7 @@ public class CommandConstants { public final static String DONE = "done."; public final static String READING_MODEL = "Reading model from %s..."; + public final static String READING_DASH_MODEL = "Reading dash model from %s... \n"; public final static String READING_TRACE = "Reading trace from %s..."; public final static String WRITING_DOT_GRAPH = "Writing DOT graph to %s..."; public final static String NO_SUCH_FILE = "%s: No such file.\n"; @@ -39,6 +40,13 @@ public class CommandConstants { "Usage: current [property]\n\n" + "By default, all properties are printed."; public final static String[] CURRENT_SHORTHAND = {"c", "curr"}; + + public final static String SHOW_NAME = "show"; + public final static String SHOW_DESCRIPTION = "Display a specified state"; + public final static String SHOW_HELP = "Display a specified state.\n\n" + + "Usage: show [state name]\n\n" + + "By default, all properties are printed."; + public final static String[] SHOW_SHORTHAND = {"s"}; public final static String HELP_NAME = "help"; public final static String HELP_DESCRIPTION = "Display the list of available commands"; @@ -49,6 +57,10 @@ public class CommandConstants { public final static String INIT_DESCRIPTION = "Return to the initial state of the active model"; public final static String INIT_HELP = "Return to the initial state of the active model.\n\nUsage: init"; public final static String[] INIT_SHORTHAND = {"i"}; + + public final static String GOTO_NAME = "goto"; + public final static String GOTO_DESCRIPTION = "Goto a specified state"; + public final static String GOTO_HELP = "Goto a specified state.\n\nUsage: goto [state name]"; public final static String LOAD_NAME = "load"; public final static String LOAD_DESCRIPTION = "Load an Alloy model"; @@ -156,4 +168,17 @@ public class CommandConstants { public final static String DOT_DESCRIPTION = "Dump DOT graph to disk"; public final static String DOT_HELP = "Dump DOT graph to the current working directory.\n\nUsage: dot"; public final static String[] DOT_SHORTHAND = {"d"}; + + public final static String TEST_NAME = "test"; + public final static String[] TEST_SHORTHAND = {"T"}; + + public final static String Force_NAME = "force"; + public final static String Force_DESCRIPTION = "force a constraint to happen in a specified number of steps (10 by default)"; + public final static String Force_HELP = "force a constraint to happen in a specified number of steps (10 by default).\\n\\nUsage: force [transition name] [max-steps]"; + + + public final static String[] Force_SHORTHAND = {"f"}; + + } + diff --git a/src/commands/CommandRegistry.java b/src/commands/CommandRegistry.java index 5865002..b1ac765 100644 --- a/src/commands/CommandRegistry.java +++ b/src/commands/CommandRegistry.java @@ -20,6 +20,9 @@ public final class CommandRegistry { new StepCommand(), new TraceCommand(), new UntilCommand(), + new ShowCommand(), + new GotoCommand(), + new ForceCommand(), }; public static Command commandForString(String string) { @@ -30,12 +33,14 @@ public static Command commandForString(String string) { if (command.getName().equals(string)) { return command; } - + String[] shorthand = command.getShorthand(); - for (String s : shorthand) { - if (s.equals(string)) { - return command; - } + if (shorthand!=null) { + for (String s : shorthand) { + if (s.equals(string)) { + return command; + } + } } } diff --git a/src/commands/CurrentCommand.java b/src/commands/CurrentCommand.java index a79fa53..3fee20c 100644 --- a/src/commands/CurrentCommand.java +++ b/src/commands/CurrentCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class CurrentCommand extends Command { @@ -22,6 +23,9 @@ public String[] getShorthand() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/DotCommand.java b/src/commands/DotCommand.java index df39ab0..1db24ba 100644 --- a/src/commands/DotCommand.java +++ b/src/commands/DotCommand.java @@ -1,6 +1,7 @@ package commands; import alloy.AlloyUtils; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.io.File; @@ -30,6 +31,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/ForceCommand.java b/src/commands/ForceCommand.java new file mode 100644 index 0000000..5b92361 --- /dev/null +++ b/src/commands/ForceCommand.java @@ -0,0 +1,60 @@ +package commands; + +import simulation.AliasManager; +import simulation.ConstraintManager; +import simulation.DashSimulationManager; +import simulation.SimulationManager; + +import java.util.Arrays; +import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class ForceCommand extends Command { + + public String getName() { + return CommandConstants.Force_NAME; + } + + public String getDescription() { + return CommandConstants.Force_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.Force_HELP; + } + + public String[] getShorthand() { + return CommandConstants.Force_SHORTHAND; + } + + public void execute(String[] input, SimulationManager simulationManager) { + + DashSimulationManager dashsimulationManager = (DashSimulationManager) simulationManager; + + + + if (input.length == 1) { + System.out.println(CommandConstants.Force_HELP); + return; + } + if (input.length == 2) { + String transitionName = input[1]; + if (dashsimulationManager.isTransition(transitionName).equals("")){ + System.out.println("transition does not exist."); + return; + } + dashsimulationManager.forceTransition(dashsimulationManager.isTransition(transitionName), 10); + } + if (input.length == 3) { + String transitionName = input[1]; + Integer max_steps = Integer.parseInt(input[2]); + if (dashsimulationManager.isTransition(transitionName).equals("")){ + System.out.println("transition does not exist."); + return; + } + dashsimulationManager.forceTransition(dashsimulationManager.isTransition(transitionName), max_steps); + } + + } +} diff --git a/src/commands/GotoCommand.java b/src/commands/GotoCommand.java new file mode 100644 index 0000000..bdbe6bd --- /dev/null +++ b/src/commands/GotoCommand.java @@ -0,0 +1,56 @@ +package commands; + +import simulation.DashSimulationManager; +import simulation.SimulationManager; + +public class GotoCommand extends Command { + public String getName() { + return CommandConstants.GOTO_NAME; + } + + public String getDescription() { + return CommandConstants.GOTO_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.GOTO_HELP; + } + + public String[] getShorthand() { + return null; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + if (input.length == 1) { + System.out.println("Illegal input. Usage: goto [state name]"); + return; + } + else { + if (input.length == 2 && input[0].equals("goto")) { + String stateName = input[1]; // + if (stateName != null && stateName.matches("[sS]\\d+")) { + int identifier = Integer.parseInt(stateName.substring(1)); + if (simulationManager.moveToState(identifier)) { + System.out.println(simulationManager.getCurrentStateString()); + return; + } + else { + System.out.println("Failed to goto state"); + } + } else { + System.out.println("Illegal input. Usage: goto [state name]"); + } + } + else { + System.out.println("Illegal input. Usage: goto [state name]"); + } + } + } +} diff --git a/src/commands/HelpCommand.java b/src/commands/HelpCommand.java index 098f220..0be2435 100644 --- a/src/commands/HelpCommand.java +++ b/src/commands/HelpCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.lang.StringBuilder; @@ -28,6 +29,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (input.length < 2) { System.out.println(getHelp()); } else { diff --git a/src/commands/HistoryCommand.java b/src/commands/HistoryCommand.java index 680e436..a5846dd 100644 --- a/src/commands/HistoryCommand.java +++ b/src/commands/HistoryCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class HistoryCommand extends Command { @@ -16,6 +17,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/InitCommand.java b/src/commands/InitCommand.java index ceb778e..803761f 100644 --- a/src/commands/InitCommand.java +++ b/src/commands/InitCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class InitCommand extends Command { @@ -20,13 +21,40 @@ public String[] getShorthand() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; } - - if (simulationManager.setToInit()) { - System.out.println(simulationManager.getCurrentStateString()); - }; + if (input.length == 1) { //if no arguments are specified, print current node + if (simulationManager.setToInit()) { + System.out.println(simulationManager.getCurrentStateString()); + }; + return; + } + else { + if (input.length == 3 && input[1].equals("goto")) { + String stateName = input[2]; // + if (stateName != null && stateName.matches("[sS]\\d+")) { + int identifier = Integer.parseInt(stateName.substring(1)); + if (simulationManager.moveToState(identifier)) { + System.out.println(simulationManager.getCurrentStateString()); + return; + } + else { + System.out.println("Failed to goto state"); + } + } else { + System.out.println("Illegal input"); + } + } + else { + //System.out.println(input.length); + //System.out.println(input[1]=="goto"); + System.out.println("Invalid command"); + } + } } } diff --git a/src/commands/LoadCommand.java b/src/commands/LoadCommand.java index e5379ab..9b618d8 100644 --- a/src/commands/LoadCommand.java +++ b/src/commands/LoadCommand.java @@ -1,6 +1,7 @@ package commands; import alloy.AlloyUtils; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.io.File; @@ -27,22 +28,45 @@ public boolean requiresFile() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (input.length < 2) { System.out.println(CommandConstants.NO_FILE_SPECIFIED); return; } - - String filename = input[1]; - File file = new File(filename); - if (!file.exists()) { - System.out.printf(CommandConstants.NO_SUCH_FILE, filename); - return; - } - - System.out.printf(CommandConstants.READING_MODEL, filename); - - if (simulationManager.initialize(file, false)) { - System.out.println(CommandConstants.DONE); + else { + if (input[1].equals("dash")||input[1].equals("-d")) { //loading dash module + if (input.length < 3) { + System.out.println(CommandConstants.NO_FILE_SPECIFIED); + return; + } + String filename = input[2]; + File file = new File(filename); + if (!file.exists()) { + System.out.printf(CommandConstants.NO_SUCH_FILE, filename); + return; + } + System.out.printf(CommandConstants.READING_DASH_MODEL, filename); + if (simulationManager.initialize(file, false)) { + System.out.println(CommandConstants.DONE); + + } + } + else { + String filename = input[1]; + File file = new File(filename); + if (!file.exists()) { + System.out.printf(CommandConstants.NO_SUCH_FILE, filename); + return; + } + + System.out.printf(CommandConstants.READING_MODEL, filename); + + if (simulationManager.initialize(file, false)) { + System.out.println(CommandConstants.DONE); + } + } } } } diff --git a/src/commands/NotFoundCommand.java b/src/commands/NotFoundCommand.java index 01a9eb8..1550936 100644 --- a/src/commands/NotFoundCommand.java +++ b/src/commands/NotFoundCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class NotFoundCommand extends Command { @@ -16,6 +17,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } System.out.printf(CommandConstants.UNDEFINED_COMMAND, input[0]); } } diff --git a/src/commands/QuitCommand.java b/src/commands/QuitCommand.java index 5c7d511..647491c 100644 --- a/src/commands/QuitCommand.java +++ b/src/commands/QuitCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class QuitCommand extends Command { @@ -21,6 +22,9 @@ public String[] getShorthand() { public void execute(String[] input, SimulationManager simulationManager) { // Only require user confirmation when they are in an active simulation. + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.exit(0); } diff --git a/src/commands/ReverseStepCommand.java b/src/commands/ReverseStepCommand.java index 3423233..fd72d19 100644 --- a/src/commands/ReverseStepCommand.java +++ b/src/commands/ReverseStepCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class ReverseStepCommand extends Command { @@ -20,6 +21,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/ScopeCommand.java b/src/commands/ScopeCommand.java index 16843f4..c5d2976 100644 --- a/src/commands/ScopeCommand.java +++ b/src/commands/ScopeCommand.java @@ -1,6 +1,7 @@ package commands; import alloy.AlloyConstants; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.util.List; @@ -20,6 +21,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/SetCommand.java b/src/commands/SetCommand.java index 0c06019..93be45d 100644 --- a/src/commands/SetCommand.java +++ b/src/commands/SetCommand.java @@ -2,6 +2,7 @@ import alloy.AlloyUtils; import alloy.ParsingConf; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.io.IOException; @@ -65,6 +66,9 @@ public void execute(String[] input, SimulationManager simulationManager) { private void setConf(String[] input, SimulationManager simulationManager) { // Omitting a filename will set the default conf. + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (input.length < 3) { System.out.print(CommandConstants.SETTING_PARSING_OPTIONS); simulationManager.setParsingConf(new ParsingConf()); diff --git a/src/commands/ShowCommand.java b/src/commands/ShowCommand.java new file mode 100644 index 0000000..b256504 --- /dev/null +++ b/src/commands/ShowCommand.java @@ -0,0 +1,47 @@ +package commands; + +import simulation.DashSimulationManager; +import simulation.SimulationManager; + +public class ShowCommand extends Command { + + + public String getName() { + return CommandConstants.SHOW_NAME; + } + + public String getDescription() { + return CommandConstants.SHOW_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.SHOW_HELP; + } + + + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + if (input.length == 1) { //if no arguments are specified, print current node + System.out.println(simulationManager.getCurrentStateString()); + return; + } + String stateName = input[1]; // + if (stateName != null && stateName.matches("[sS]\\d+")) { + int identifier = Integer.parseInt(stateName.substring(1)); + //update control states graph here + if (simulationManager instanceof DashSimulationManager) { + DashSimulationManager dashSimManager = (DashSimulationManager) simulationManager; + } + + System.out.println(simulationManager.getStateString(identifier)); + return; + } else { + System.out.println("Illegal input"); + } + } +} diff --git a/src/commands/StepCommand.java b/src/commands/StepCommand.java index 3f3b33e..4859ba7 100644 --- a/src/commands/StepCommand.java +++ b/src/commands/StepCommand.java @@ -1,6 +1,7 @@ package commands; import simulation.AliasManager; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.util.ArrayList; @@ -8,15 +9,13 @@ import java.util.List; public class StepCommand extends Command { - private final static String[] SHORTHAND = CommandConstants.STEP_SHORTHAND; + public String getName() { return CommandConstants.STEP_NAME; } - public String[] getShorthand() { - return SHORTHAND; - } + public String getDescription() { return CommandConstants.STEP_DESCRIPTION; @@ -27,11 +26,14 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { - if (!simulationManager.isInitialized()) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } + if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; } - + int steps = 1; List constraints = new ArrayList(); diff --git a/src/commands/TraceCommand.java b/src/commands/TraceCommand.java index 0e8dc49..997ea33 100644 --- a/src/commands/TraceCommand.java +++ b/src/commands/TraceCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; import java.io.File; @@ -28,6 +29,9 @@ public boolean requiresFile() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (input.length < 2) { System.out.println(CommandConstants.NO_FILE_SPECIFIED); return; diff --git a/src/commands/UntilCommand.java b/src/commands/UntilCommand.java index eb02da5..6ca8f65 100644 --- a/src/commands/UntilCommand.java +++ b/src/commands/UntilCommand.java @@ -1,5 +1,6 @@ package commands; +import simulation.DashSimulationManager; import simulation.SimulationManager; public class UntilCommand extends Command { @@ -20,6 +21,9 @@ public String getHelp() { } public void execute(String[] input, SimulationManager simulationManager) { + if (simulationManager instanceof DashSimulationManager) { + simulationManager = (DashSimulationManager) simulationManager; + } if (!simulationManager.isInitialized()) { System.out.println(CommandConstants.NO_MODEL_LOADED); return; diff --git a/src/commands/readme.md b/src/commands/readme.md new file mode 100644 index 0000000..031128b --- /dev/null +++ b/src/commands/readme.md @@ -0,0 +1,22 @@ +# Commands Package README + +## Overview + +This package contains files that implement aldb commands. + +## Contents + +### 1. `Command.java` +- **Purpose:** + - This class defines the structure of command objects. + +### 2. `CommandConstants.java` +- **Purpose:** + - This class contains string constants used by commands. + + +### 3. Other .java files +- **Purpose:** + - Each .java file implements the corresponding command by parsing input and calling functions in simulationManager for specific operations. + + \ No newline at end of file diff --git a/src/core/AlloyGUI.java b/src/core/AlloyGUI.java new file mode 100644 index 0000000..25f6cf3 --- /dev/null +++ b/src/core/AlloyGUI.java @@ -0,0 +1,100 @@ +package core; +import javax.swing.*; + +import org.json.JSONObject; +import java.awt.*; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.logging.Level; +import java.util.logging.Logger; +import simulation.SimulationManager; + +public class AlloyGUI { + private JsonDrawing drawingPanel; + private String jsonFilePath; + private SimulationManager simulationManager; + + public AlloyGUI(String filePath,SimulationManager s) { + simulationManager = s; + this.jsonFilePath = filePath; + initUI(); + } + + private void initUI() { + SwingUtilities.invokeLater(() -> { + try { + // Load JSON content + String content = new String(Files.readAllBytes(Paths.get(jsonFilePath))); + JSONObject graphData = new JSONObject(content); + + // Create and set up the frame + JFrame frame = new JFrame("JSON Viewer"); + frame.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); + frame.setLayout(new BorderLayout()); + + // Create and add the drawing panel + drawingPanel = new JsonDrawing(graphData,simulationManager); + frame.add(drawingPanel, BorderLayout.CENTER); + + // Set up frame size and visibility + frame.setSize(1000, 1000); + frame.setVisible(true); + + } catch (IOException e) { + Logger.getLogger(getClass().getName()).log(Level.SEVERE, "Error loading JSON file", e); + JOptionPane.showMessageDialog( null, "Error loading JSON file: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); + } + }); + } + + // Method to refresh the painting + public void refreshJson() { + + SwingUtilities.invokeLater(() -> { + try { + // Load new JSON content + String content = new String(Files.readAllBytes(Paths.get(jsonFilePath))); + JSONObject newGraphData = new JSONObject(content); + + + SwingUtilities.invokeLater(() -> { + drawingPanel.updateGraphData(newGraphData); + drawingPanel.repaint(); + }); + + } catch (IOException e) { + Logger.getLogger(getClass().getName()).log(Level.SEVERE, "Error loading new JSON file", e); + JOptionPane.showMessageDialog(null, "Error loading new JSON file: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); + } + }); + } + + public void refreshJsonWithDelay(int delayMillis) { + System.out.println("refreshing..."); + Timer timer = new Timer(delayMillis, e -> { + try { + // Load new JSON content + String content = new String(Files.readAllBytes(Paths.get(jsonFilePath))); + JSONObject newGraphData = new JSONObject(content); + + SwingUtilities.invokeLater(() -> { + drawingPanel.updateGraphData(newGraphData); + drawingPanel.repaint(); + }); + + } catch (IOException e1) { + Logger.getLogger(getClass().getName()).log(Level.SEVERE, "Error loading new JSON file", e1); + JOptionPane.showMessageDialog(null, "Error loading new JSON file: " + e1.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); + } + }); + + timer.setRepeats(false); // Ensures the Timer runs only once + timer.start(); // Start the timer + } +} + + + + + diff --git a/src/core/DashGUI.java b/src/core/DashGUI.java new file mode 100644 index 0000000..01fab21 --- /dev/null +++ b/src/core/DashGUI.java @@ -0,0 +1,114 @@ +package core; +import javax.swing.*; + +import org.json.JSONObject; + +import simulation.SimulationManager; + +import java.awt.*; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.util.logging.Level; +import java.util.logging.Logger; + +public class DashGUI { + private JsonDrawing drawingPanel1; + private JsonDrawing drawingPanel2; + private String jsonFilePath1; + private String jsonFilePath2; + private SimulationManager simulationManager; + + public DashGUI(String filePath1, String filePath2, SimulationManager s) { + this.jsonFilePath1 = filePath1; + this.jsonFilePath2 = filePath2; + simulationManager = s; + initUI(); + } + + private void initUI() { + SwingUtilities.invokeLater(() -> { + try { + // Load JSON content + String content1 = new String(Files.readAllBytes(Paths.get(jsonFilePath1))); + JSONObject graphData1 = new JSONObject(content1); + + String content2 = new String(Files.readAllBytes(Paths.get(jsonFilePath2))); + JSONObject graphData2 = new JSONObject(content2); + + // Create and set up the frame + JFrame frame = new JFrame("Dash Model Viewer"); + frame.setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); + frame.setLayout(new GridLayout(1, 2)); // Two panels side by side + + // Create and add the drawing panels + drawingPanel1 = new JsonDrawing(graphData1,simulationManager); + drawingPanel2 = new JsonDrawing(graphData2,simulationManager); + frame.add(drawingPanel1); + frame.add(drawingPanel2); + + // Set up frame size and visibility + frame.setSize(1000, 500); // Adjusted to accommodate two panels + frame.setVisible(true); + + } catch (IOException e) { + Logger.getLogger(getClass().getName()).log(Level.SEVERE, "Error loading JSON file", e); + JOptionPane.showMessageDialog(null, "Error loading JSON file: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); + } + }); + } + + // Method to refresh the painting + public void refreshJson() { + SwingUtilities.invokeLater(() -> { + try { + // Load new JSON content + String content1 = new String(Files.readAllBytes(Paths.get(jsonFilePath1))); + JSONObject newGraphData1 = new JSONObject(content1); + + String content2 = new String(Files.readAllBytes(Paths.get(jsonFilePath2))); + JSONObject newGraphData2 = new JSONObject(content2); + + SwingUtilities.invokeLater(() -> { + drawingPanel1.updateGraphData(newGraphData1); + drawingPanel1.repaint(); + + drawingPanel2.updateGraphData(newGraphData2); + drawingPanel2.repaint(); + }); + + } catch (IOException e) { + Logger.getLogger(getClass().getName()).log(Level.SEVERE, "Error loading new JSON file", e); + JOptionPane.showMessageDialog(null, "Error loading new JSON file: " + e.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); + } + }); + } + + public void refreshJsonWithDelay(int delayMillis) { + Timer timer = new Timer(delayMillis, e -> { + try { + // Load new JSON content + String content1 = new String(Files.readAllBytes(Paths.get(jsonFilePath1))); + JSONObject newGraphData1 = new JSONObject(content1); + + String content2 = new String(Files.readAllBytes(Paths.get(jsonFilePath2))); + JSONObject newGraphData2 = new JSONObject(content2); + + SwingUtilities.invokeLater(() -> { + drawingPanel1.updateGraphData(newGraphData1); + drawingPanel1.repaint(); + + drawingPanel2.updateGraphData(newGraphData2); + drawingPanel2.repaint(); + }); + + } catch (IOException e1) { + Logger.getLogger(getClass().getName()).log(Level.SEVERE, "Error loading new JSON file", e1); + JOptionPane.showMessageDialog(null, "Error loading new JSON file: " + e1.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); + } + }); + + timer.setRepeats(false); // Ensures the Timer runs only once + timer.start(); // Start the timer + } +} diff --git a/src/core/DashImageDisplay.java b/src/core/DashImageDisplay.java new file mode 100644 index 0000000..753eb96 --- /dev/null +++ b/src/core/DashImageDisplay.java @@ -0,0 +1,113 @@ +package core; + +import javax.swing.*; +import java.awt.*; +import java.io.File; +import java.io.IOException; +import javax.imageio.ImageIO; +import java.awt.image.BufferedImage; + +public class DashImageDisplay extends JFrame { + private BufferedImage image1; + private BufferedImage image2; + private JLabel imageLabel1; + private JLabel imageLabel2; + + public DashImageDisplay() { + setTitle("Image Display"); + setSize(800, 600); + setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); + setLocationRelativeTo(null); + + // Load the images + loadImages(); + + // Create labels to display the images + imageLabel1 = new JLabel(new ImageIcon(image1)); + imageLabel2 = new JLabel(new ImageIcon(image2)); + + // Create a panel with a GridLayout to hold the image labels + JPanel panel = new JPanel(new GridLayout(2, 1)); + panel.add(imageLabel1); + panel.add(imageLabel2); + + // Add the panel to the JFrame + add(panel, BorderLayout.CENTER); + } + + private void loadImages() { + waitForFinalFiles("state_tree.png", "control_states.png"); + + try { + // Load the final image files + File file1 = new File("state_tree.png"); + File file2 = new File("control_states.png"); + + if (file1.exists() && file1.isFile()) { + image1 = ImageIO.read(file1); + } + + if (file2.exists() && file2.isFile()) { + image2 = ImageIO.read(file2); + } + } catch (IOException e) { + e.printStackTrace(); + System.exit(1); // Exit if loading fails + } + } + + private void waitForFinalFiles(String... filePaths) { + for (String filePath : filePaths) { + File finalFile = new File(filePath); + long startTime = System.currentTimeMillis(); + long timeout = 10000; // 10 seconds + + while (System.currentTimeMillis() - startTime < timeout) { + if (finalFile.exists() && finalFile.isFile()) { + break; // File exists, proceed + } + + try { + Thread.sleep(100); // Check every 100 milliseconds + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + + if (!finalFile.exists()) { + System.out.println("Timeout reached: " + filePath + " not found within 10 seconds."); + } + } + } + + public void refresh() { + new Thread(() -> { + waitForFinalFiles("state_tree.png", "control_states.png"); + + SwingUtilities.invokeLater(() -> { + loadImages(); + imageLabel1.setIcon(new ImageIcon(image1)); + imageLabel2.setIcon(new ImageIcon(image2)); + }); + }).start(); + } + + public static void writeImage(BufferedImage image, String path) { + File tempFile = new File(path + "_temp.png"); + File finalFile = new File(path); + + try { + // Write to the temporary file first + ImageIO.write(image, "png", tempFile); + + // Rename to the final file after writing is complete + if (tempFile.renameTo(finalFile)) { + System.out.println("File written and renamed successfully."); + } else { + System.out.println("Error renaming the file."); + } + } catch (IOException e) { + e.printStackTrace(); + } + } +} diff --git a/src/core/ImageDisplay.java b/src/core/ImageDisplay.java new file mode 100644 index 0000000..e93bc28 --- /dev/null +++ b/src/core/ImageDisplay.java @@ -0,0 +1,111 @@ +package core; + +import javax.swing.*; +import java.awt.*; +import java.io.File; +import java.io.IOException; +import javax.imageio.ImageIO; +import java.awt.image.BufferedImage; + +public class ImageDisplay extends JFrame { + private BufferedImage image1; + private BufferedImage image2; + private JLabel imageLabel1; + private JLabel imageLabel2; + + public ImageDisplay() { + setTitle("Image Display"); + setSize(800, 600); + setDefaultCloseOperation(JFrame.EXIT_ON_CLOSE); + setLocationRelativeTo(null); + + // Load the images + loadImages(); + + // Create labels to display the images + imageLabel1 = new JLabel(new ImageIcon(image1)); + + + // Create a panel with a GridLayout to hold the image labels + JPanel panel = new JPanel(new GridLayout(1, 1)); + panel.add(imageLabel1); + + + // Add the panel to the JFrame + add(panel, BorderLayout.CENTER); + } + + private void loadImages() { + waitForFinalFiles("state_tree.png", "control_states.png"); + + try { + // Load the final image files + File file1 = new File("state_tree.png"); + + + if (file1.exists() && file1.isFile()) { + image1 = ImageIO.read(file1); + } + + + } catch (IOException e) { + e.printStackTrace(); + System.exit(1); // Exit if loading fails + } + } + + private void waitForFinalFiles(String... filePaths) { + for (String filePath : filePaths) { + File finalFile = new File(filePath); + long startTime = System.currentTimeMillis(); + long timeout = 10000; // 10 seconds + + while (System.currentTimeMillis() - startTime < timeout) { + if (finalFile.exists() && finalFile.isFile()) { + break; // File exists, proceed + } + + try { + Thread.sleep(100); // Check every 100 milliseconds + } catch (InterruptedException e) { + e.printStackTrace(); + } + } + + if (!finalFile.exists()) { + System.out.println("Timeout reached: " + filePath + " not found within 10 seconds."); + } + } + } + + public void refresh() { + new Thread(() -> { + waitForFinalFiles("state_tree.png", "control_states.png"); + + SwingUtilities.invokeLater(() -> { + loadImages(); + imageLabel1.setIcon(new ImageIcon(image1)); + + }); + }).start(); + } + + public static void writeImage(BufferedImage image, String path) { + File tempFile = new File(path + "_temp.png"); + File finalFile = new File(path); + + try { + // Write to the temporary file first + ImageIO.write(image, "png", tempFile); + + // Rename to the final file after writing is complete + if (tempFile.renameTo(finalFile)) { + System.out.println("File written and renamed successfully."); + } else { + System.out.println("Error renaming the file."); + } + } catch (IOException e) { + e.printStackTrace(); + } + } +} diff --git a/src/core/JsonDrawing.java b/src/core/JsonDrawing.java new file mode 100644 index 0000000..d56cc81 --- /dev/null +++ b/src/core/JsonDrawing.java @@ -0,0 +1,515 @@ + +package core; + +import org.json.JSONArray; +import org.json.JSONObject; + +import simulation.SimulationManager; + +import javax.swing.*; +import java.awt.*; +import java.awt.event.*; +import java.awt.geom.Ellipse2D; +import java.awt.geom.Path2D; +import java.awt.geom.Point2D; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; + +public class JsonDrawing extends JPanel { + private JSONArray objects; + private List shapeList = new ArrayList<>(); + private Map shapeLabelMap = new LinkedHashMap<>(); + + private ShapeInfo hoveredShape = null; + private Integer graphWidth; + private JSONArray edges; + + private boolean isDrawingVisible = true; + private double zoomFactor = 1.0; + private boolean isDragging = false; + private int lastX, lastY; + private SimulationManager simulationManager; + + public JsonDrawing(JSONObject graphData,SimulationManager sm) { + simulationManager = sm; + if (graphData.has("objects")) { + objects = graphData.getJSONArray("objects"); + JSONArray graphInfo = graphData.getJSONArray("_draw_"); + + JSONObject s = graphInfo.getJSONObject(2); + JSONArray points = s.getJSONArray("points"); + JSONArray secondPoint = points.getJSONArray(1); + graphWidth = (int) secondPoint.getDouble(1); + if (graphData.has("edges")) { + edges = graphData.getJSONArray("edges"); + } + } + // Add mouse listener for click and hover events + addMouseListener(new MouseAdapter() { + @Override + public void mousePressed(MouseEvent e) { + if (SwingUtilities.isRightMouseButton(e)) { + isDragging = true; + isDrawingVisible = false; + lastX = e.getX(); + lastY = e.getY(); + } + } + + @Override + public void mouseReleased(MouseEvent e) { + if (SwingUtilities.isRightMouseButton(e)) { + isDragging = false; + isDrawingVisible = true; + setCursor(Cursor.getDefaultCursor()); + repaint(); + } + } + + @Override + public void mouseClicked(MouseEvent e) { + Point2D.Double adjustedClickPoint = new Point2D.Double( + e.getX() / zoomFactor, + e.getY() / zoomFactor + ); + if (SwingUtilities.isLeftMouseButton(e) && !isDragging) { + //printShapeLabelMap(); + + // Iterate over shapeList in reverse order to find the topmost shape + for (int i = shapeList.size() - 1; i >= 0; i--) { + ShapeInfo shapeInfo = shapeList.get(i); + if (shapeInfo.shape.contains(adjustedClickPoint)) { + String label = shapeLabelMap.get(shapeInfo); + JOptionPane.showMessageDialog(JsonDrawing.this, "Shape clicked: " + shapeInfo + ", Label: " + label); + simulationManager.handleClick(label); + break; // Stop after finding the topmost shape + } + } + } + } + + + }); + + addMouseMotionListener(new MouseMotionAdapter() { + @Override + public void mouseMoved(MouseEvent e) { + boolean repaintNeeded = false; + for (ShapeInfo shapeInfo : shapeList) { + if (shapeInfo.shape.contains(e.getPoint())) { + if (hoveredShape != shapeInfo) { + hoveredShape = shapeInfo; + repaintNeeded = true; + } + } else if (hoveredShape == shapeInfo) { + hoveredShape = null; + repaintNeeded = true; + } + } + if (repaintNeeded) { + repaint(); + } + } + + @Override + public void mouseDragged(MouseEvent e) { + if (SwingUtilities.isRightMouseButton(e)) { + setCursor(Cursor.getPredefinedCursor(Cursor.MOVE_CURSOR)); + int dx = e.getX() - lastX; + int dy = e.getY() - lastY; + lastX = e.getX(); + lastY = e.getY(); + setLocation(getX() + dx, getY() + dy); + repaint(); // Continuously repaint as the mouse is dragging + } + } + }); + + // Add mouse wheel listener for zooming + addMouseWheelListener(e -> { + if (e.getWheelRotation() < 0) { + zoomIn(); + } else { + zoomOut(); + } + }); + } + + private void zoomIn() { + zoomFactor += 0.1; + repaint(); + } + + private void zoomOut() { + zoomFactor -= 0.1; + repaint(); + } + + @Override + protected void paintComponent(Graphics g) { + super.paintComponent(g); + Graphics2D g2d = (Graphics2D) g; + + if (isDrawingVisible) { + shapeList.clear(); + shapeLabelMap.clear(); // Clear the map before adding new entries + g2d.scale(zoomFactor, zoomFactor); + + for (int i = 0; i < objects.length(); i++) { + JSONObject s = objects.getJSONObject(i); + String fillcolor = ""; + if (s.has("fillcolor")) { + fillcolor = s.getString("fillcolor"); + } + if (s.has("_draw_")) { + JSONArray shapeInfoArray = s.getJSONArray("_draw_"); + drawShapes(g2d, shapeInfoArray, fillcolor); + } + if (s.has("_ldraw_")) { + JSONArray labelInfoArray = s.getJSONArray("_ldraw_"); + drawLabels(g2d, labelInfoArray); + } + } + if (edges != null) { + for (int i = 0; i < edges.length(); i++) { + JSONObject s = edges.getJSONObject(i); + String fillcolor = ""; + if (s.has("fillcolor")) { + fillcolor = s.getString("fillcolor"); + } + if (s.has("_draw_")) { + JSONArray shapeInfoArray = s.getJSONArray("_draw_"); + drawShapes(g2d, shapeInfoArray, fillcolor); + } + if (s.has("_hdraw_")) { + JSONArray headInfoArray = s.getJSONArray("_hdraw_"); + drawShapes(g2d, headInfoArray, fillcolor); + } + if (s.has("_ldraw_")) { + JSONArray labelInfoArray = s.getJSONArray("_ldraw_"); + drawLabels(g2d, labelInfoArray); + } + } + } + } + } + + private void drawShapes(Graphics2D g2d, JSONArray shapeInfoArray, String fillcolor) { + for (int i = 0; i < shapeInfoArray.length(); i++) { + JSONObject jsonObject = shapeInfoArray.getJSONObject(i); + String op = jsonObject.getString("op"); + + switch (op) { + case "C": + break; + case "c": + // Handle color or other properties + if (jsonObject.has("color")) { + Color color = Color.decode(jsonObject.getString("color")); + g2d.setColor(color); + } + break; + case "e": + // Draw ellipse + if (jsonObject.has("rect")) { + JSONArray rectArray = jsonObject.getJSONArray("rect"); + int x = rectArray.getInt(0); + int y = graphWidth - rectArray.getInt(1); + int width = rectArray.getInt(2); + int height = rectArray.getInt(3); + + // Convert centroid to upper-left corner + int upperLeftX = x - (width / 2); + int upperLeftY = y - (height / 2); + Ellipse2D ellipse = new Ellipse2D.Double(upperLeftX, upperLeftY, width, height); + ShapeInfo shapeInfo = new ShapeInfo(ellipse, g2d.getColor()); + shapeList.add(shapeInfo); + shapeLabelMap.put(shapeInfo, null); // Assume null label for now + + // Add shading effect if hovered + if (hoveredShape != null && hoveredShape.shape.equals(ellipse)) { + g2d.setColor(hoveredShape.color.darker()); + } + g2d.draw(ellipse); + if (fillcolor.equals("yellow")) { + g2d.setColor(Color.YELLOW); + g2d.fill(ellipse); + } + g2d.setColor(hoveredShape != null && hoveredShape.shape.equals(ellipse) ? hoveredShape.color : g2d.getColor()); + } + break; + case "p": + // Draw polygon + if (jsonObject.has("points")) { + JSONArray pointArray = jsonObject.getJSONArray("points"); + Polygon polygon = new Polygon(); + for (int j = 0; j < pointArray.length(); j++) { + JSONArray point = pointArray.getJSONArray(j); + int x = point.getInt(0); + int y = graphWidth - point.getInt(1); + polygon.addPoint(x, y); + } + ShapeInfo shapeInfo = new ShapeInfo(polygon, g2d.getColor()); + shapeList.add(shapeInfo); + shapeLabelMap.put(shapeInfo, null); // Assume null label for now + + if (hoveredShape != null && hoveredShape.shape.equals(polygon)) { + g2d.setColor(Color.GREEN); + } + g2d.draw(polygon); + if (fillcolor.equals("yellow")) { + g2d.setColor(Color.YELLOW); + g2d.fill(polygon); + } + } + break; + case "b": + // Draw path + if (jsonObject.has("points")) { + JSONArray pointArray = jsonObject.getJSONArray("points"); + Path2D path = new Path2D.Double(); + boolean firstPoint = true; + for (int j = 0; j < pointArray.length(); j++) { + JSONArray point = pointArray.getJSONArray(j); + double x = point.getDouble(0); + double y = graphWidth - point.getDouble(1); + if (firstPoint) { + path.moveTo(x, y); + firstPoint = false; + } else { + path.lineTo(x, y); + } + } + ShapeInfo shapeInfo = new ShapeInfo(path, g2d.getColor()); + shapeList.add(shapeInfo); + shapeLabelMap.put(shapeInfo, null); // Assume null label for now + g2d.draw(path); + } + break; + case "P": + // Draw polygon + if (jsonObject.has("points")) { + JSONArray pointArray = jsonObject.getJSONArray("points"); + if (pointArray.length() == 4) { // rectangle + Polygon rectangle = new Polygon(); + int x1 = pointArray.getJSONArray(0).getInt(0); + int x2 = pointArray.getJSONArray(1).getInt(0); + int x3 = pointArray.getJSONArray(2).getInt(0); + int x4 = pointArray.getJSONArray(3).getInt(0); + int y1 = graphWidth - pointArray.getJSONArray(0).getInt(1); + int y2 = graphWidth - pointArray.getJSONArray(1).getInt(1); + int y3 = graphWidth - pointArray.getJSONArray(2).getInt(1); + int y4 = graphWidth - pointArray.getJSONArray(3).getInt(1); + rectangle.addPoint(x1, y1); + rectangle.addPoint(x2, y2); + rectangle.addPoint(x3, y3); + rectangle.addPoint(x4, y4); + + ShapeInfo shapeInfo = new ShapeInfo(rectangle, g2d.getColor()); + shapeList.add(shapeInfo); + shapeLabelMap.put(shapeInfo, null); // Assume null label for now + + g2d.draw(rectangle); + if (fillcolor.equals("yellow")) { + g2d.setColor(Color.YELLOW); + g2d.fill(rectangle); + } + } + + if (pointArray.length() == 3) { // triangle, head of an edge + Polygon triangle = new Polygon(); + int x1 = pointArray.getJSONArray(0).getInt(0); + int x2 = pointArray.getJSONArray(1).getInt(0); + int x3 = pointArray.getJSONArray(2).getInt(0); + int y1 = graphWidth - pointArray.getJSONArray(0).getInt(1); + int y2 = graphWidth - pointArray.getJSONArray(1).getInt(1); + int y3 = graphWidth - pointArray.getJSONArray(2).getInt(1); + triangle.addPoint(x1, y1); + triangle.addPoint(x2, y2); + triangle.addPoint(x3, y3); + g2d.fill(triangle); + } + } + break; + case "S": + break; + case "E": + if (jsonObject.has("rect")) { + JSONArray rectArray = jsonObject.getJSONArray("rect"); + int x = rectArray.getInt(0); + int y = graphWidth - rectArray.getInt(1); + int width = rectArray.getInt(2); + int height = rectArray.getInt(3); + + // Convert centroid to upper-left corner + int upperLeftX = x - (width / 2); + int upperLeftY = y - (height / 2); + Ellipse2D ellipse = new Ellipse2D.Double(upperLeftX, upperLeftY, width, height); + ShapeInfo shapeInfo = new ShapeInfo(ellipse, g2d.getColor()); + shapeList.add(shapeInfo); + shapeLabelMap.put(shapeInfo, null); // Assume null label for now + + // Add shading effect if hovered + if (hoveredShape != null && hoveredShape.shape.equals(ellipse)) { + g2d.setColor(hoveredShape.color.darker()); + } + g2d.draw(ellipse); + if (fillcolor.equals("yellow")) { + g2d.setColor(Color.YELLOW); + g2d.fill(ellipse); + } + g2d.setColor(hoveredShape != null && hoveredShape.shape.equals(ellipse) ? hoveredShape.color : g2d.getColor()); + } + break; + default: + throw new IllegalArgumentException("Unsupported operation: " + op); + } + } + } + + private void drawLabels(Graphics2D g2d, JSONArray labelInfoArray) { + for (int i = 0; i < labelInfoArray.length(); i++) { + JSONObject jsonObject = labelInfoArray.getJSONObject(i); + String op = jsonObject.getString("op"); + + switch (op) { + case "F": + // Set font properties + if (jsonObject.has("face") && jsonObject.has("size")) { + String face = jsonObject.getString("face"); + int size = jsonObject.getInt("size"); + g2d.setFont(new Font(face, Font.PLAIN, size)); + } + break; + case "c": + // Handle color or other properties + if (jsonObject.has("color")) { + Color color = Color.decode(jsonObject.getString("color")); + g2d.setColor(color); + } + break; + case "T": + // Draw text + if (jsonObject.has("pt") && jsonObject.has("text")) { + JSONArray ptArray = jsonObject.getJSONArray("pt"); + int x = ptArray.getInt(0); + int y = ptArray.getInt(1); + String text = jsonObject.getString("text"); + FontMetrics metrics = g2d.getFontMetrics(g2d.getFont()); + int textWidth = metrics.stringWidth(text); + int textHeight = metrics.getHeight(); + int textAscent = metrics.getAscent(); + + // Calculate the new x and y coordinates + int adjustedX = x - textWidth / 2; + int adjustedY = y + textAscent / 2 - textHeight / 2; + + + // Draw the string at the adjusted coordinates + g2d.drawString(text, adjustedX, graphWidth - adjustedY); + + // Update the label for the corresponding shape + updateLastValue(shapeLabelMap,text); + + Rectangle textBox = new Rectangle(adjustedX, graphWidth- adjustedY - textAscent, textWidth, textHeight); + ShapeInfo shapeInfo = new ShapeInfo(textBox, g2d.getColor()); + //g2d.draw(textBox); + shapeLabelMap.put(shapeInfo,text); + shapeList.add(shapeInfo); + } + break; + default: + throw new IllegalArgumentException("Unsupported operation: " + op); + } + } + } + + + private ShapeInfo getLastKey(Map map) { + // Convert the key set to a list + List keys = new ArrayList<>(map.keySet()); + + // Return the last key in the list + if (!keys.isEmpty()) { + return keys.get(keys.size() - 1); + } + return null; // Return null if the map is empty + } + + private void updateLastValue(Map map, String newValue) { + ShapeInfo lastKey = getLastKey(map); + if (lastKey != null) { + map.put(lastKey, newValue); + } else { + System.out.println("Map is empty, no update performed."); + } + } + + public void updateGraphData(JSONObject newGraphData) { + if (!newGraphData.has("objects")) { + return; + } + objects = newGraphData.getJSONArray("objects"); + JSONArray graphInfo = newGraphData.getJSONArray("_draw_"); + + JSONObject s = graphInfo.getJSONObject(2); + JSONArray points = s.getJSONArray("points"); + JSONArray secondPoint = points.getJSONArray(1); + graphWidth = (int) secondPoint.getDouble(1); + + if (newGraphData.has("edges")) { + edges = newGraphData.getJSONArray("edges"); + } else { + edges = null; + } + + // Rebuild shape list and label map based on new data + shapeList.clear(); + shapeLabelMap.clear(); + repaint(); // Trigger a repaint to reflect the new data + } + + // Inner class to hold shape information + private static class ShapeInfo { + Shape shape; + Color color; + + ShapeInfo(Shape shape, Color color) { + this.shape = shape; + this.color = color; + } + + @Override + public String toString() { + return "ShapeInfo{" + + "shape=" + shape + + ", color=" + color + + '}'; + } + + @Override + public boolean equals(Object obj) { + if (this == obj) return true; + if (obj == null || getClass() != obj.getClass()) return false; + ShapeInfo shapeInfo = (ShapeInfo) obj; + return shape.equals(shapeInfo.shape); + } + + @Override + public int hashCode() { + return shape.hashCode(); + } + } + + private void printShapeLabelMap() { + System.out.println("Shape Label Map:"); + for (Map.Entry entry : shapeLabelMap.entrySet()) { + ShapeInfo shapeInfo = entry.getKey(); + String label = entry.getValue(); + System.out.println("Shape: " + shapeInfo + ", Label: " + (label != null ? label : "No Label")); + } + } +} diff --git a/src/core/Main.java b/src/core/Main.java index c506b66..f62b049 100644 --- a/src/core/Main.java +++ b/src/core/Main.java @@ -3,6 +3,7 @@ import commands.Command; import commands.CommandConstants; import commands.CommandRegistry; +import simulation.DashSimulationManager; import simulation.SimulationManager; import net.sourceforge.argparse4j.ArgumentParsers; import net.sourceforge.argparse4j.impl.Arguments; @@ -14,7 +15,10 @@ public class Main { private static SimulationManager simulationManager; + private static DashSimulationManager dashsimulationManager; private static SessionLog log; + + private static String SET_MODE_PROMPT = "Enter 'd' or 'dash' to enter dash mode. Enter anything else to enter alloy mode."; private static String prevSessionLogPath; private static String PROGRAM_NAME = "Alloy Debugger (ALDB)"; @@ -44,7 +48,8 @@ public static void main(String[] args) throws IOException { parser.addArgument(VERSION_FLAG_SHORT, VERSION_FLAG).help(VERSION_DESC).action(Arguments.version()); parser.addArgument(RESTORE_FLAG_SHORT, RESTORE_FLAG).help(RESTORE_DESC); parser.addArgument(FILE_ARG_NAME).nargs(OPTIONAL).help(FILE_ARG_DESC); - + + boolean dashmode = false; Namespace ns = null; try { ns = parser.parseArgs(args); @@ -54,8 +59,11 @@ public static void main(String[] args) throws IOException { } simulationManager = new SimulationManager(); + dashsimulationManager = new DashSimulationManager(); CLI cli = new CLI(); - + + //your code here + // Pre-load a model if its path is passed in on start-up. String modelPath = ns.getString(FILE_ARG_NAME); if (modelPath != null) { @@ -85,10 +93,26 @@ public static void main(String[] args) throws IOException { prevLog.restore(simulationManager, log); } } - + System.out.println(SET_MODE_PROMPT); + String[] modeinput = cli.getInput(); + if (modeinput.length > 0 && (modeinput[0].equals("d") || modeinput[0].equals("dash"))) { + dashmode = true; + System.out.println("Dash mode activated."); + } + else { + System.out.println("Alloy mode activated."); + } while (true) { String[] input = cli.getInput(); + Command command = CommandRegistry.commandForString(input[0]); + if (dashmode) { + command.execute(input, dashsimulationManager); + if (log.isInitialized()) { + log.append(input); + } + continue; + } command.execute(input, simulationManager); if (log.isInitialized()) { log.append(input); diff --git a/src/core/readme.md b/src/core/readme.md new file mode 100644 index 0000000..0cace6a --- /dev/null +++ b/src/core/readme.md @@ -0,0 +1,27 @@ +# Core Package README + +## Overview + +This package contains core files that implement aldb and visualizing components. + +## Contents + +### 1. `Main.java` +- **Purpose:** + - Starts the aldb CLI. + +### 2. `CLI.java` +- **Purpose:** + - Parses user input into commands. + +### 3. `AlloyGUI.java` `DashGUI.java` +- **Purpose:** + - Implements the GUI for .als file input and .dsh file input respectively. + +### 4. `ImageDisplay.java` +- **Purpose:** + - Opens a window displaying the images generated in each step. + +### 5. `JsonDrawing.java` +- **Purpose:** + - Reads .json files generated during simulation, extracts layout information and generates interactive graphs. \ No newline at end of file diff --git a/src/simulation/DashSimulationManager.java b/src/simulation/DashSimulationManager.java new file mode 100644 index 0000000..92f4d04 --- /dev/null +++ b/src/simulation/DashSimulationManager.java @@ -0,0 +1,1189 @@ +package simulation; +import core.DashGUI; +import core.DashImageDisplay; +import core.ImageDisplay; +import core.JsonDrawing; +import core.AlloyGUI; +import state.StateGraph; +import state.StateNode; +import state.StatePath; + +import alloy.AlloyConstants; +import alloy.AlloyInterface; +import alloy.AlloyUtils; +import alloy.ParsingConf; +import alloy.SigData; +import ca.uwaterloo.watform.core.DashUtilFcns; +import ca.uwaterloo.watform.mainfunctions.MainFunctions; +import ca.uwaterloo.watform.parser.DashModule; +import commands.CommandConstants; +import edu.mit.csail.sdg.alloy4.A4Reporter; +import edu.mit.csail.sdg.alloy4.Err; +import edu.mit.csail.sdg.ast.Sig; +import edu.mit.csail.sdg.parser.CompModule; +import edu.mit.csail.sdg.translator.A4Solution; +import edu.mit.csail.sdg.translator.A4Tuple; + +import java.io.IOException; +import java.io.BufferedWriter; +import java.io.File; +import java.io.FileWriter; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.nio.file.StandardCopyOption; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; +import java.util.Map; +import java.util.SortedMap; +import java.util.Stack; +import java.util.TreeMap; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import org.json.JSONObject; +import org.yaml.snakeyaml.error.YAMLException; +import javax.swing.*; +public class DashSimulationManager extends SimulationManager{ + private final static String TEMP_FILENAME_PREFIX = "_tmp_"; + + private File alloyModelFile; + private String alloyModelString; + private String alloyInitString; + private SortedMap> scopes; + private ParsingConf persistentParsingConf; // Set by set conf - used across multiple models. + private ParsingConf embeddedParsingConf; // Set by load - used for the current model only. + private SigData stateSigData; + private StatePath statePath; + private StateGraph stateGraph; + private Stack activeSolutions; + private AliasManager aliasManager; + private ConstraintManager constraintManager; + private GraphPrinter gp; + private ImageDisplay display; + private DashImageDisplay dashdisplay; + private boolean traceMode; + private boolean diffMode; + private DashModule d;// Whether differential output is enabled. + private DashGUI dashGUI; + + public DashSimulationManager() { + scopes = new TreeMap<>(); + statePath = new StatePath(); + stateGraph = new StateGraph(); + persistentParsingConf = new ParsingConf(); + embeddedParsingConf = null; + activeSolutions = new Stack<>(); + aliasManager = new AliasManager(); + constraintManager = new ConstraintManager(); + traceMode = false; + diffMode = true; + + } + + // checks if a given label represents a state, e.g. is s/S followed by a digit + public boolean isState(String label) { + String regex = "^[sS]\\d+$"; + Pattern pattern = Pattern.compile(regex); + Matcher matcher = pattern.matcher(label); + return matcher.matches(); + } + + //Dash-specific checks if a given label represents a transition + public String isTransition(String label) { + List transitions = d.getAllTransNames(); + for (String transition : transitions) { + + if (label.equals(formatString(transition))) { + return formatString(transition); + } + } + return ""; + } + + + //implements logic for handling clicks on transitions/states in GUI + public void handleClick(String label) { // + + if ((isState(label))) { + String identifier = label.substring(1); + moveToState(Integer.parseInt(identifier)); + return; + } + if (!isTransition(label).equals("")) { + + + int limit = 10; + + if (!forceTransition(isTransition(label),limit)) { + System.out.println(CommandConstants.UNTIL_FAILED); + } + return; + } + } + + + //Dash-specific, given a transitionName and step size, add alloy predicate to force the transition be taken within the specified number of steps + public boolean forceTransition(String transitionName,int limit) { + String breakPredicate = AlloyUtils.getTransitionPredicate(transitionName); + + for (int steps = 1; steps <= limit; steps++) { + try { + String curInitString; + if (stateGraph.size() > 1) { + curInitString = statePath.getCurNode().getAlloyInitString(); + } else { + curInitString = alloyInitString; + } + //System.out.println( AlloyUtils.annotatedTransitionSystemForced(alloyModelString + curInitString + breakPredicate, getParsingConf(), steps)); + AlloyUtils.writeToFile( + AlloyUtils.annotatedTransitionSystemForced(alloyModelString + curInitString + breakPredicate, getParsingConf(), steps), + alloyModelFile + ); + } catch (IOException e) { + return false; + } + + CompModule compModule = null; + try { + compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + } catch (Err e) { + return false; + } + + A4Solution sol = null; + try { + sol = AlloyInterface.run(compModule); + } catch (Err e) { + return false; + } + + if (!sol.satisfiable()) { + // Breakpoints not hit for current step size. Try next step size. + continue; + } + + statePath.commitNodes(); + + StateNode startNode = statePath.getCurNode(); + + List stateNodes = getStateNodesForA4Solution(sol); + stateNodes.remove(0); + + statePath.setTempPath(stateNodes); + + stateGraph.addNodes(startNode, stateNodes); + + this.activeSolutions.clear(); + this.activeSolutions.push(sol); + + savePath(stateNodes); + updateHierarchy(); + printGraph(); + loadImage(); + loadDash(); + //statePath.printPath(); + //stateGraph.printGraph(); + return true; + } + System.out.println("Unable to force transition within specified number of steps."); + return false; + } + + + + + public void showDashGUI() { // Dash-specific, starts/refreshes the GUI displaying the interactive state tree and the control states graph + + if (dashGUI==null) { + dashGUI = new DashGUI("state_tree.json","control_states.json",this); + dashGUI.refreshJsonWithDelay(1000); + return; + } + dashGUI.refreshJsonWithDelay(1000); + + } + + public void savePath() { //saves the path for the current node + if (statePath.getCurNode()!=null) { + StateNode curr_node_from_path = statePath.getCurNode(); + StateNode curr_node=stateGraph.getNodeById(curr_node_from_path.getIdentifier()); + if (curr_node.getPath().size()==0) { + curr_node.storePath(statePath.getPath()); + //System.out.println(curr_node.getPath()); + } + } + } + + //Dash-specific, saves the path for a given list of nodes, used in forceTransitions + public void savePath(List nodes) { + for (StateNode node : nodes) { + List targetPath = statePath.getPath(); + int index = targetPath.indexOf(node.getIdentifier()); + //System.out.println("saving: node "+node.getIdentifier()+" "+targetPath.subList(0, index+1)); + node.storePath(targetPath.subList(0, index+1)); + } + } + + //builds the .dot file using the information stored in stateGraph and generates the .png image + public void printGraph() { + gp = new GraphPrinter(); + for (int i = 0; i < stateGraph.size(); i++) { + StateNode node = stateGraph.getNode(i); + if (node.getSteps().size()!=0) { + for (StateNode next_node : node.getSteps()) { + if (next_node.getTransitionName().isEmpty()) { + gp.addln("S"+Integer.toString(node.getIdentifier()) + " -> " + "S"+Integer.toString(next_node.getIdentifier())); + } + else { + gp.addln("S"+Integer.toString(node.getIdentifier()) + " -> " + "S"+Integer.toString(next_node.getIdentifier())+"[label="+next_node.getTransitionName() +"]"); + } + + } + } + else { + gp.addln("S"+Integer.toString(node.getIdentifier())); + } + if (node.hasStable()) { + if (node.getStable()) { + gp.addln("S"+Integer.toString(node.getIdentifier()) + "[color=green]"); + } + else { + gp.addln("S"+Integer.toString(node.getIdentifier()) + "[color=red]"); + } + } + } + if (statePath.getCurNode()!=null) { + StateNode curr_node = statePath.getCurNode(); + gp.addln("S"+Integer.toString(curr_node.getIdentifier())+ "[style=filled, fillcolor=yellow]"); //highlight curr node + + + } + gp.print("state_tree"); + gp.generateJson("state_tree"); + + } + + public void loadImage() { + if (this.dashdisplay==null) { + this.dashdisplay=new DashImageDisplay(); + } + dashdisplay.refresh(); + dashdisplay.setVisible(true); + + } + + public boolean isTrace() { + return traceMode; + } + + public void setDiffMode(boolean b) { + diffMode = b; + } + + public boolean isDiffMode() { + return diffMode; + } + + /** + * isInitialized returns True iff a model or trace has been loaded. + * @return boolean + */ + public boolean isInitialized() { + return !statePath.isEmpty(); + } + + public void setParsingConf(ParsingConf conf) { + persistentParsingConf = conf; + } + + // move to a specified state using the state path stored (which represents the first route taken to reach the state) + public boolean moveToState(int identifier) { + if (identifier > stateGraph.size()) { + return false; + } + else { + List targetpath = new ArrayList<>(); + StateNode targetnode = stateGraph.getNodeById(identifier); + for (int i : targetnode.getPath()) { + targetpath.add(stateGraph.getNodeById(i)); + } + statePath.setPath(targetpath); + printGraph(); + loadImage(); + loadDash(); + updateHierarchy(); + return true; + } + } + /** + * initialize is a wrapper for initializing a model or trace which cleans up internal state if + * initialization fails. + * @return boolean + */ + public boolean initialize(File file, boolean isTrace) { + ParsingConf oldEmbeddedParsingConf = embeddedParsingConf; + + if (file.getName().substring(file.getName().lastIndexOf('.') + 1).equals("dsh")) { + boolean res = initializeDashModel(file); + return res; + } + else { + System.out.println("Currently in dash mode, file with .dsh extension expected."); + return false; + } + + + } + + //Dash-specific, takes a .dsh file, translate it to .als and loads it in aldb + public boolean initializeDashModel(File file) { + A4Reporter rep = new A4Reporter(); + d = MainFunctions.parseAndResolveDashFile(file.getPath(),rep); + //buildHierarchy(d,rootName,gp,null); + + //addTransitions(gp); + + //translate to alloy + //initializeWithModel(file); + try { + //d = MainFunctions.resolveDash(d, rep); + System.out.println("Resolved Dash"); + CompModule c = MainFunctions.translate(d, rep); + System.out.println("Translated Dash to Alloy"); + System.out.println("Method: " + "traces" +"\n"); + String filename=file.getName(); + String outfilename = filename.substring(0,filename.length()-4) + "-" + "traces" + ".als"; + File out = new File(outfilename); + if (!out.exists()) out.createNewFile(); + System.out.println("Creating: " + outfilename); + FileWriter fw = new FileWriter(out.getAbsoluteFile()); + BufferedWriter bw = new BufferedWriter(fw); + bw.write(d.toStringAlloy()); + bw.close(); + System.out.println("Done!"); + initializeWithModel(out); + + } + catch (Exception e) { + DashUtilFcns.handleException(e); + } + + + //showTransitions(); + //gp.print("control_states"); + printGraph(); + savePath(); + + updateHierarchy(); + loadImage(); + loadDash(); + + return true; + } + + + //Dash-specific, helper function for getting max depth of the control state tree + public static int maxDepth(DashModule d,String root) { + if (root == null) { + return 0; + } + if (d.getImmChildren(root).isEmpty()) { + return 1; + } + int maxDepth = 0; + for (String child : d.getImmChildren(root)) { + maxDepth = Math.max(maxDepth, maxDepth(d,child)); + } + return maxDepth + 1; + } + + //Dash-specific, helper function for finding depth of a given node + public static int findNodeDepth(String targetnode, DashModule d) { + String root=d.getRootName(); + return findNodeDepthHelper(root, targetnode, 1, d); + } + + //Dash-specific, helper function for finding depth of a given node + private static int findNodeDepthHelper(String root, String targetnode, int depth, DashModule d) { + if (root == null) { + return -1; // Node not found + } + if (root.equals(targetnode)) { + return depth; + } + for (String child : d.getImmChildren(root)) { + int childDepth = findNodeDepthHelper(child, targetnode, depth + 1, d); + if (childDepth != -1) { + return childDepth; + } + } + return -1; // Node not found in this subtree + } + + + //Dash-specific, function for creating the .dot file for the control state graph + public void buildHierarchy(DashModule d, String nodeName,GraphPrinter gp, List highlightedStates) { + + //System.out.println("visiting node "+nodeName); + //System.out.println(nodeName+" is leaf:"+d.isLeaf(nodeName)); + //System.out.println(nodeName+" depth:"+findNodeDepth(nodeName,d)); + //System.out.println("max depth:"+maxDepth(d,d.getRootName())); + if (!d.isLeaf(nodeName) || findNodeDepth(nodeName,d)!=maxDepth(d,d.getRootName())) { + if (d.isRoot(nodeName)) { + gp.addln("subgraph cluster_"+formatString(nodeName)+" {"); + gp.addln("label="+formatString(nodeName)); + if (d.isAnd(nodeName)) { + gp.addln("style=dashed"); + } + + } + else { + gp.addln("subgraph cluster_"+formatString(nodeName)+" {"); + if (highlightedStates!=null && highlightedStates.contains(formatString(nodeName))) { + gp.addln("style=filled"); + gp.addln("fillcolor=yellow"); + } + gp.addln("label="+formatString(nodeName).substring(formatString(nodeName).lastIndexOf('_')+1)); + gp.addln(formatString(nodeName)+" [style=invis,shape=point, penwidth=0]"); + if (d.isAnd(nodeName)) { + gp.addln("style=dashed"); + } + } + } + else { + if (highlightedStates!=null && highlightedStates.contains(formatString(nodeName))) { + gp.addln(formatString(nodeName)+" [label="+formatString(nodeName).substring(formatString(nodeName).lastIndexOf('_') + 1)+", style=filled, fillcolor=yellow"+"]"); + } + else { + gp.addln(formatString(nodeName)+" [label="+formatString(nodeName).substring(formatString(nodeName).lastIndexOf('_') + 1)+"]"); + } + } + List children = d.getImmChildren(nodeName); + for (String child : children) { + buildHierarchy(d, child,gp,highlightedStates); + } + + if (!d.isLeaf(nodeName)|| findNodeDepth(nodeName,d)!=maxDepth(d,d.getRootName())) { + if (!d.isRoot(nodeName)) { + gp.addln(formatString(nodeName)+"_other_side [style=invis,shape=point,penwidth=0]"); + } + gp.addln("}"); + } + } + + //Dash-specific, prints out all transitions + public void showTransitions() { + List transitions = d.getAllTransNames(); + for (String transition : transitions) { + System.out.println("transition: "+transition); + System.out.println("source: "+d.getTransSrc(transition)); + System.out.println("destination: "+d.getTransDest(transition)); + } + } + + //Dash-specific, adds transitions (edges) to the control state graph + public void addTransitions(GraphPrinter gp) { + List transitions = d.getAllTransNames(); + for (String transition : transitions) { + //String[] parts = transition.split("/"); + //String lastPart = parts[parts.length - 1]; + String source = d.getTransSrc(transition).toString(); + String destination = d.getTransDest(transition).toString(); + if (findNodeDepth(source,d)==maxDepth(d,d.getRootName())){ //is node + gp.addln(formatString(source)+"->"+formatString(destination)+" [label="+formatString(transition)+"]"); + } + else { //is subgraph + gp.addln(formatString(source)+"->"+formatString(destination)+"_other_side"+" [label="+formatString(transition)+",ltail=cluster_"+formatString(source)+",lhead=cluster_"+formatString(destination)+",]"); + } + } + } + + //Dash-specific, updates the control state .dot file + public void updateHierarchy() { + gp = new GraphPrinter(); + + + if (statePath.getCurNode()!=null) { + + StateNode curr_node = statePath.getCurNode(); + List controlstates=curr_node.getControlStateNames(); + buildHierarchy(d, d.getRootName(), gp,controlstates); + } + + addTransitions(gp); + gp.print("control_states"); + gp.generateJson("control_states"); + + + } + + public void loadDash() { + showDashGUI(); + dashdisplay.refresh(); + dashdisplay.setVisible(true); + } + + //Dash-specific, updates the control state .dot file and highlights current node + public void updateHierarchy(int id) { + gp = new GraphPrinter(); + + + if (statePath.getNode(id-1)!=null) { + StateNode curr_node = statePath.getNode(id-1); + List controlstates=curr_node.getControlStateNames(); + buildHierarchy(d, d.getRootName(), gp,controlstates); + } + gp.print("control_states"); + gp.generateJson("control_states"); + showDashGUI(); + dashdisplay.refresh(); + dashdisplay.setVisible(true); + } + + // replace the '/'s in dash states and transitions with '_' + public String formatString(String s) { + return s.replace('/', '_'); + } + /** + * performReverseStep goes backward by `steps` states in the current state traversal path. + * @param steps + */ + public void performReverseStep(int steps) { + int initialPos = statePath.getPosition(); + StateNode targetNode = statePath.getNode(initialPos < steps ? 0 : initialPos - steps); + + if (initialPos <= steps) { + setToInit(); + } else { + // To set the internal state properly for an alternate path to be selected, perform + // a step from the position one step behind the expected final position. + statePath.decrementPosition(steps + 1, traceMode); + performStep(1); + } + + // If the user was on some alternate path, we need to perform `alt` until we get back + // to the correct StateNode. + while (!statePath.getCurNode().equals(targetNode)) { + selectAlternatePath(false); + } + + // Ensure the ID is set when reverse-stepping back to an alternative initial state. + statePath.getCurNode().setIdentifier(targetNode.getIdentifier()); + //statePath.printPath(); + updateHierarchy(); + printGraph(); + loadImage(); + loadDash(); + savePath(); + } + + /** + * performStep steps the transition system forward by `steps` state transitions. + * @param steps + * @return boolean + */ + public boolean performStep(int steps) { + return performStep(steps, new ArrayList()); + } + + /** + * performStep steps the transition system forward by `steps` state transitions. + * The i-th constraint in `constraints` is applied to the i-th transition. + * @param steps + * @param constraints + * @return boolean + */ + public boolean performStep(int steps, List constraints) { + if (isTrace()) { + if (statePath.atEnd()) { + System.out.println("Cannot perform step. End of trace reached."); + return false; + } + statePath.incrementPosition(steps); + return true; + } + + statePath.commitNodes(); + + + String pathPredicate = AlloyUtils.getPathPredicate(constraints, stateSigData); + try { + String curInitString; + if (stateGraph.size() > 1) { + curInitString = statePath.getCurNode().getAlloyInitString(); + } else { + curInitString = alloyInitString; + } + AlloyUtils.writeToFile( + AlloyUtils.annotatedTransitionSystemStep(alloyModelString + curInitString + pathPredicate, getParsingConf(), steps), + alloyModelFile + ); + } catch (IOException e) { + System.out.println("Cannot perform step. I/O failed."); + return false; + } + + CompModule compModule = null; + try { + compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + } catch (Err e) { + System.out.println("Cannot perform step. Internal error."); + return false; + } + + A4Solution sol = null; + try { + sol = AlloyInterface.run(compModule); + } catch (Err e) { + System.out.println("Cannot perform step. Internal error."); + return false; + } + + if (!sol.satisfiable()) { + System.out.println("Cannot perform step. Transition constraint is unsatisfiable."); + return false; + } + + StateNode startNode = statePath.getCurNode(); + + // For steps > 1, we need to generate all nodes representing the path that the series of state transitions + // takes within the state graph. + List stateNodes = getStateNodesForA4Solution(sol); + + // Filter out the initial node to avoid re-adding it to statePath. + stateNodes.remove(0); + statePath.setTempPath(stateNodes); + + stateGraph.addNodes(startNode, stateNodes); + + this.activeSolutions.clear(); + this.activeSolutions.push(sol); + //statePath.printPath(); + printGraph(); + loadImage(); + loadDash(); + savePath(); + return true; + } + + public boolean selectAlternatePath(boolean reverse) { + if (activeSolutions.isEmpty()) { + return false; + } + + A4Solution activeSolution = null; + if (reverse) { + if (activeSolutions.size() == 1) { + return false; + } + + activeSolutions.pop(); + activeSolution = activeSolutions.peek(); + } else { + activeSolution = activeSolutions.peek(); + if (!activeSolution.next().satisfiable()) { + return false; + } + + activeSolution = activeSolution.next(); + activeSolutions.push(activeSolution); + } + + List stateNodes = getStateNodesForA4Solution(activeSolution); + StateNode startNode = stateNodes.get(0); + stateNodes.remove(0); + + statePath.clearTempPath(); + if (stateNodes.isEmpty()) { + // This branch should only be reached when an alternate path + // is selected for an initial state. + statePath.setTempPath(Arrays.asList(startNode)); + } else { + statePath.setTempPath(stateNodes); + } + + stateGraph.addNodes(startNode, stateNodes); + //statePath.printPath(); + + printGraph(); + updateHierarchy(); + loadImage(); + loadDash(); + savePath(); + return true; + } + + /** + * performUntil steps the transition system up to `limit` state transitions, + * until at least one of the constraints in the breakpoint list is satisfied. + * @param limit + * @return boolean + */ + public boolean performUntil(int limit) { + String breakPredicate = AlloyUtils.getBreakPredicate(constraintManager.getConstraints(), stateSigData); + + for (int steps = 1; steps <= limit; steps++) { + try { + String curInitString; + if (stateGraph.size() > 1) { + curInitString = statePath.getCurNode().getAlloyInitString(); + } else { + curInitString = alloyInitString; + } + AlloyUtils.writeToFile( + AlloyUtils.annotatedTransitionSystemUntil(alloyModelString + curInitString + breakPredicate, getParsingConf(), steps), + alloyModelFile + ); + } catch (IOException e) { + return false; + } + + CompModule compModule = null; + try { + compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + } catch (Err e) { + return false; + } + + A4Solution sol = null; + try { + sol = AlloyInterface.run(compModule); + } catch (Err e) { + return false; + } + + if (!sol.satisfiable()) { + // Breakpoints not hit for current step size. Try next step size. + continue; + } + + statePath.commitNodes(); + + StateNode startNode = statePath.getCurNode(); + + List stateNodes = getStateNodesForA4Solution(sol); + stateNodes.remove(0); + statePath.setTempPath(stateNodes); + + stateGraph.addNodes(startNode, stateNodes); + + this.activeSolutions.clear(); + this.activeSolutions.push(sol); + updateHierarchy(); + printGraph(); + loadImage(); + loadDash(); + savePath(); + return true; + } + return false; + } + + /** + * setToInit sets SimulationManager's internal state to point to the initial state of the + * active model or trace. + * @return boolean + */ + public boolean setToInit() { + if (traceMode) { + statePath.decrementPosition(statePath.getPosition(), traceMode); + return true; + } + try { + AlloyUtils.writeToFile( + AlloyUtils.annotatedTransitionSystem( + this.alloyModelString + this.alloyInitString, + getParsingConf(), + 0 + ), + alloyModelFile + ); + } catch (IOException e) { + System.out.println("error. I/O failed, cannot re-initialize model."); + return false; + } + + CompModule compModule = null; + try { + compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + } catch (Err e) { + System.out.println("internal error."); + return false; + } + + A4Solution sol = null; + try { + sol = AlloyInterface.run(compModule); + } catch (Err e) { + System.out.println("internal error."); + return false; + } + + List initialNodes = getStateNodesForA4Solution(sol); + // We don't re-add this initial node to the StateGraph, so manually set its identifier here. + initialNodes.get(0).setIdentifier(1); + + statePath.clearPath(); + statePath.setTempPath(initialNodes); + + activeSolutions.clear(); + activeSolutions.push(sol); + updateHierarchy(); + printGraph(); + loadImage(); + loadDash(); + return true; + } + + /** + * validateConstraint validates a user-entered constraint by transforming + * the constraint into a predicate and verifying that the model compiles + * after the introduction of the new predicate. + * @param String constraint + * @return boolean + */ + public boolean validateConstraint(String constraint) { + String breakPredicate = AlloyUtils.getBreakPredicate(Arrays.asList(constraint), stateSigData); + + + try { + AlloyUtils.writeToFile( + alloyModelString + alloyInitString + breakPredicate, + alloyModelFile + ); + } catch (IOException e) { + return false; + } + + try { + AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + } catch (Err e) { + return false; + } + + return true; + } + + public String getDOTString() { + return stateGraph.getDOTString(); + } + + public String getHistory(int n) { + return statePath.getHistory(n, traceMode); + } + + public Map> getScopes() { + return scopes; + } + + public List getScopeForSig(String sigName) { + return scopes.get(sigName); + } + + public String getStateString(int id) { + if (id<=0 || id-1>stateGraph.size()) { + return "state not found!"; + } + return stateGraph.getNode(id-1).toString(); + } + + public String getCurrentStateString() { + return statePath.getCurNode().toString(); + } + + public String getCurrentStateStringForProperty(String property) { + return statePath.getCurNode().stringForProperty(property); + } + + /** + * getCurrentStateDiffStringFromLastCommit returns the diff between the current + * and the previous last-committed state. + * @return String + */ + public String getCurrentStateDiffStringFromLastCommit() { + StateNode prev = statePath.getNode(statePath.getPosition() - statePath.getTempPathSize()); + return statePath.getCurNode().getDiffString(prev); + } + + /** + * getCurrentStateDiffStringByDelta returns the diff between the current state + * and the state at the (current - delta) position in the path. + * @param int delta + * @return String + */ + public String getCurrentStateDiffStringByDelta(int delta) { + StateNode prev = statePath.getNode(statePath.getPosition() - delta); + return statePath.getCurNode().getDiffString(prev); + } + + public AliasManager getAliasManager() { + return aliasManager; + } + + public ConstraintManager getConstraintManager() { + return constraintManager; + } + + public String getWorkingDirPath() { + return System.getProperty("user.dir"); + } + + private boolean initializeWithModel(File model) { + try { + AlloyInterface.compile(model.getPath()); + } catch (Err e) { + System.out.printf("error.\n\n%s\n", e.toString()); + return false; + } + + String tempModelFilename = TEMP_FILENAME_PREFIX + model.getName(); + // Note that the temp model file must be created in the same directory as the input model + // in order for Alloy to correctly find imported submodules. + File tempModelFile = new File(model.getParentFile(), tempModelFilename); + tempModelFile.deleteOnExit(); + + try { + Files.copy(model.toPath(), tempModelFile.toPath(), StandardCopyOption.REPLACE_EXISTING); + } catch (Exception e) { + System.out.println("error. I/O failed."); + return false; + } + + alloyModelFile = tempModelFile; + + String modelString; + try { + modelString = AlloyUtils.readFromFile(alloyModelFile); + } catch (IOException e) { + System.out.println("error. Failed to read file."); + return false; + } + + String configString = ParsingConf.getConfStringFromFileString(modelString).trim(); + if (!configString.isEmpty()) { + try { + embeddedParsingConf = ParsingConf.initializeWithYaml(configString); + } catch (YAMLException e) { + System.out.println("error. Invalid configuration."); + return false; + } + } + + int transRelIndex = modelString.indexOf(String.format("pred %s", getParsingConf().getTransitionRelationName())); + if (transRelIndex == -1) { + System.out.printf("error. Predicate %s not found.\n", getParsingConf().getTransitionRelationName()); + return false; + } + + int initStartIndex = modelString.indexOf(String.format("pred %s", getParsingConf().getInitPredicateName())); + if (initStartIndex == -1) { + System.out.printf("error. Predicate %s not found.\n", getParsingConf().getInitPredicateName()); + return false; + } + + // Count the number of BLOCK_INITIALIZERs and BLOCK_TERMINATORs to + // determine the end of the init predicate. + int blocks = 0; + int initEndIndex = -1; + for (int i = initStartIndex; i < modelString.length(); i++) { + String c = String.valueOf(modelString.charAt(i)); + if (c.equals(AlloyConstants.BLOCK_INITIALIZER)) { + blocks += 1; + } else if (c.equals(AlloyConstants.BLOCK_TERMINATOR)) { + blocks -= 1; + if (blocks == 0) { + // When all blocks are closed, the end of the predicate has + // been found. + initEndIndex = i; + break; + } else if (blocks < 0) { + // More BLOCK_TERMINATORs than BLOCK_INITIALIZERs is a + // syntax error. + break; + } + } + } + + if (initEndIndex == -1) { + System.out.printf("error. Issue parsing predicate %s.\n", getParsingConf().getInitPredicateName()); + return false; + } + + this.alloyInitString = modelString.substring(initStartIndex, initEndIndex + 1); + this.alloyModelString = + modelString.substring(0, initStartIndex) + + AlloyUtils.getConcreteSigsDefinition(getParsingConf().getAdditionalSigScopes()) + + modelString.substring(initEndIndex + 1, modelString.length()); + + try { + AlloyUtils.writeToFile( + AlloyUtils.annotatedTransitionSystem( + this.alloyModelString + this.alloyInitString, + getParsingConf(), + 0 + ), + alloyModelFile + ); + } catch (IOException e) { + System.out.println("error. I/O failed, cannot initialize model."); + return false; + } + + CompModule compModule = null; + try { + compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + } catch (Err e) { + System.out.println("internal error."); + return false; + } + + A4Solution sol = null; + try { + sol = AlloyInterface.run(compModule); + } catch (Err e) { + System.out.printf("error.\n\n%s\n", e.msg.trim()); + return false; + } + + if (!sol.satisfiable()) { + System.out.println("error. No instance found. Predicate may be inconsistent."); + return false; + } + + evaluateScopes(sol); + + Sig stateSig = AlloyInterface.getSigFromA4Solution(sol, getParsingConf().getStateSigName()); + if (stateSig == null) { + System.out.printf("error. Sig %s not found.\n", getParsingConf().getStateSigName()); + return false; + } + //System.out.println(getParsingConf().getStateSigName()); + + stateSigData = new SigData(stateSig); + + List initialNodes = getStateNodesForA4Solution(sol); + statePath.clearPath(); + statePath.setTempPath(initialNodes); + stateGraph.initWithNodes(initialNodes); + + this.traceMode = false; + this.activeSolutions.clear(); + this.activeSolutions.push(sol); + + return true; + } + + private boolean initializeWithTrace(File trace) { + A4Solution sol; + try { + sol = AlloyInterface.solutionFromXMLFile(trace); + } catch (Err e) { + System.out.printf("error.\n\n%s\n", e.toString()); + return false; + } catch (Exception e) { + System.out.println("error. Could not read XML file."); + return false; + } + + evaluateScopes(sol); + + Sig stateSig = AlloyInterface.getSigFromA4Solution(sol, getParsingConf().getStateSigName()); + if (stateSig == null) { + System.out.printf("error. Sig %s not found.\n", getParsingConf().getStateSigName()); + return false; + } + + stateSigData = new SigData(stateSig); + + List stateNodes = getStateNodesForA4Solution(sol); + if (stateNodes.isEmpty()) { + System.out.println("internal error."); + return false; + } + + statePath.initWithPath(stateNodes); + statePath.setPosition(0); + stateGraph.initWithNodes(stateNodes); + + this.traceMode = true; + this.activeSolutions.clear(); + + return true; + } + + private List getStateNodesForA4Solution(A4Solution sol) { + List stateNodes = new ArrayList<>(); + + Sig stateSig = AlloyInterface.getSigFromA4Solution(sol, getParsingConf().getStateSigName()); + if (stateSig == null) { + return stateNodes; + } + + if (stateSigData == null) { + stateSigData = new SigData(stateSig); + } + + int steps = sol.eval(stateSig).size(); + for (int i = 0; i < steps; i++) { + stateNodes.add(new StateNode(stateSigData, getParsingConf())); + } + + for (Sig.Field field : stateSig.getFields()) { + for (A4Tuple tuple : sol.eval(field)) { + String atom = tuple.atom(0); + StateNode node = stateNodes.get( + Integer.parseInt(atom.split(AlloyConstants.ALLOY_ATOM_SEPARATOR)[1]) + ); + String tupleString = tuple.toString(); + node.addValueToField( + field.label, + tupleString + .substring( + tupleString.indexOf(AlloyConstants.SET_DELIMITER) + 2, tupleString.length() + ) + // Sigs will only ever have $0 as a suffix since we control their scope. + .replace(AlloyConstants.VALUE_SUFFIX, "") + ); + } + } + + return stateNodes; + } + + /** + * evaluateScopes gets the scope for each reachable sig for an A4Solution and stores it in StateGraph. + * @param A4Solution sol + */ + private void evaluateScopes(A4Solution sol) { + for (Sig s : sol.getAllReachableSigs()) { + String label = s.label; + if (label.startsWith(AlloyConstants.THIS)) { + label = label.substring(AlloyConstants.THIS.length()); + } + // Ignore the 'univ' sig which itself contains the scope of the entire model. + if (label.equals(AlloyConstants.UNIV)) { + continue; + } + // Ignore internal concrete sigs that we've injected into the model. + else if (label.matches(AlloyConstants.CONCRETE_SIG_REGEX)) { + int i = label.indexOf(AlloyConstants.UNDERSCORE); + String origSigName = label.substring(0, i); + Map sigScopes = getParsingConf().getAdditionalSigScopes(); + if (sigScopes.containsKey(origSigName) && + Integer.parseInt(label.substring(i + 1)) < sigScopes.get(origSigName)) { + continue; + } + } + List tuples = new ArrayList<>(); + for (A4Tuple t : sol.eval(s)) { + tuples.add(t.toString().replace(AlloyConstants.VALUE_SUFFIX, "")); + } + scopes.put(label, tuples); + } + } + + private ParsingConf getParsingConf() { + return embeddedParsingConf != null ? embeddedParsingConf : persistentParsingConf; + } +} diff --git a/src/simulation/GraphPrinter.java b/src/simulation/GraphPrinter.java new file mode 100644 index 0000000..3fb5920 --- /dev/null +++ b/src/simulation/GraphPrinter.java @@ -0,0 +1,93 @@ +package simulation; +import java.io.FileOutputStream; +import java.io.IOException; + +public class GraphPrinter { + + private StringBuilder graphBuilder = new StringBuilder(); + private String filePrefix; + + public GraphPrinter() {} + + /** + * @param filePrefix Only put filename prefix E.g. File1, File2, MyNewFile, myfile etc. It will use the filePrefix to create output dot file and png file with same name. + */ + public GraphPrinter(String filePrefix) { + this.filePrefix = filePrefix; + } + + /** + * @param line line contains a valid dot file graphviz text + */ + public void addln(String line) { + graphBuilder.append(line).append("\n"); + } + + public void add(String text) { + graphBuilder.append(text); + } + + public void addnewln() { + graphBuilder.append("\n"); + } + + /** + * Creates an output dot file and uses that to create graphviz png output using following command + * dot -Tpng .dot -o .png + * If you want to change the certain format, change below. + */ + public void print(String prefix) { + try { + filePrefix = prefix; + if (prefix.equals("control_states")) { + graphBuilder.insert(0, "compound=true \n"); + } + graphBuilder.insert(0, "digraph G {").append("\n"); + + graphBuilder.append("}").append("\n"); + writeTextToFile(filePrefix + ".dot", graphBuilder.toString()); + + StringBuilder command = new StringBuilder(); + command.append("dot -Tpng "). // output type + append(filePrefix).append(".dot "). // input dot file + append("-o ").append(filePrefix).append(".png"); // output image + + executeCommand(command.toString()); + } catch (Exception ex) { + ex.printStackTrace(); + } + } + + + public void generateJson(String prefix) { + //System.out.println("generating Json..."); + try { + filePrefix = prefix; + + StringBuilder command = new StringBuilder(); + command.append("dot -Tjson "). // output type + append(filePrefix).append(".dot "). // input dot file + append("-o ").append(filePrefix).append(".json"); // output json + //System.out.println(command.toString()); + executeCommand(command.toString()); + } catch (Exception ex) { + ex.printStackTrace(); + } + } + + + private void executeCommand(String command) throws Exception { + Process process = Runtime.getRuntime().exec(command); + int exitCode = process.waitFor(); + if (exitCode != 0) { + throw new RuntimeException("Command execution failed with exit code: " + exitCode); + } + } + + + private void writeTextToFile(String fileName, String text) throws IOException { + FileOutputStream outputStream = new FileOutputStream(fileName); + outputStream.write(text.getBytes()); + outputStream.close(); + } +} \ No newline at end of file diff --git a/src/simulation/SimulationManager.java b/src/simulation/SimulationManager.java index e5e9824..ebfbd29 100644 --- a/src/simulation/SimulationManager.java +++ b/src/simulation/SimulationManager.java @@ -1,5 +1,9 @@ package simulation; - +import core.DashGUI; +import core.DashImageDisplay; +import core.ImageDisplay; +import core.JsonDrawing; +import core.AlloyGUI; import state.StateGraph; import state.StateNode; import state.StatePath; @@ -9,7 +13,11 @@ import alloy.AlloyUtils; import alloy.ParsingConf; import alloy.SigData; - +import ca.uwaterloo.watform.core.DashUtilFcns; +import ca.uwaterloo.watform.mainfunctions.MainFunctions; +import ca.uwaterloo.watform.parser.DashModule; +import commands.CommandConstants; +import edu.mit.csail.sdg.alloy4.A4Reporter; import edu.mit.csail.sdg.alloy4.Err; import edu.mit.csail.sdg.ast.Sig; import edu.mit.csail.sdg.parser.CompModule; @@ -17,8 +25,11 @@ import edu.mit.csail.sdg.translator.A4Tuple; import java.io.IOException; +import java.io.BufferedWriter; import java.io.File; +import java.io.FileWriter; import java.nio.file.Files; +import java.nio.file.Paths; import java.nio.file.StandardCopyOption; import java.util.ArrayList; import java.util.Arrays; @@ -27,9 +38,12 @@ import java.util.SortedMap; import java.util.Stack; import java.util.TreeMap; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import org.json.JSONObject; import org.yaml.snakeyaml.error.YAMLException; - +import javax.swing.*; public class SimulationManager { private final static String TEMP_FILENAME_PREFIX = "_tmp_"; @@ -45,10 +59,16 @@ public class SimulationManager { private Stack activeSolutions; private AliasManager aliasManager; private ConstraintManager constraintManager; - + private GraphPrinter gp; + private ImageDisplay display; + private AlloyGUI stateTreeViewer; private boolean traceMode; - private boolean diffMode; // Whether differential output is enabled. - + private boolean diffMode; + + + + + public SimulationManager() { scopes = new TreeMap<>(); statePath = new StatePath(); @@ -58,11 +78,104 @@ public SimulationManager() { activeSolutions = new Stack<>(); aliasManager = new AliasManager(); constraintManager = new ConstraintManager(); - traceMode = false; diffMode = true; + } - + + // checks if a given label represents a state, e.g. is s/S followed by a digit + public boolean isState(String label) { + String regex = "^[sS]\\d+$"; + Pattern pattern = Pattern.compile(regex); + Matcher matcher = pattern.matcher(label); + return matcher.matches(); + } + + + + //implements logic for handling clicks on transitions/states in GUI + public void handleClick(String label) { // + + if ((isState(label))) { + String identifier = label.substring(1); + moveToState(Integer.parseInt(identifier)); + return; + } + + } + + + public void savePath() { //saves the path for the current node + if (statePath.getCurNode()!=null) { + StateNode curr_node_from_path = statePath.getCurNode(); + StateNode curr_node=stateGraph.getNodeById(curr_node_from_path.getIdentifier()); + if (curr_node.getPath().size()==0) { + curr_node.storePath(statePath.getPath()); + //System.out.println(curr_node.getPath()); + } + } + } + + //builds the .dot file using the information stored in stateGraph and generates the .png image + public void printGraph() { + gp = new GraphPrinter(); + for (int i = 0; i < stateGraph.size(); i++) { + StateNode node = stateGraph.getNode(i); + if (node.getSteps().size()!=0) { + for (StateNode next_node : node.getSteps()) { + if (next_node.getTransitionName().isEmpty()) { + gp.addln("S"+Integer.toString(node.getIdentifier()) + " -> " + "S"+Integer.toString(next_node.getIdentifier())); + } + else { + gp.addln("S"+Integer.toString(node.getIdentifier()) + " -> " + "S"+Integer.toString(next_node.getIdentifier())+"[label="+next_node.getTransitionName() +"]"); + } + + } + } + else { + gp.addln("S"+Integer.toString(node.getIdentifier())); + } + if (node.hasStable()) { + if (node.getStable()) { + gp.addln("S"+Integer.toString(node.getIdentifier()) + "[color=green]"); + } + else { + gp.addln("S"+Integer.toString(node.getIdentifier()) + "[color=red]"); + } + } + } + if (statePath.getCurNode()!=null) { + StateNode curr_node = statePath.getCurNode(); + gp.addln("S"+Integer.toString(curr_node.getIdentifier())+ "[style=filled, fillcolor=yellow]"); //highlight curr node + + + } + gp.print("state_tree"); + gp.generateJson("state_tree"); + + } + + public void showStateTreeJson() { // starts/refreshes the GUI displaying the interactive state tree + + if (stateTreeViewer==null) { + stateTreeViewer = new AlloyGUI("state_tree.json",this); + stateTreeViewer.refreshJsonWithDelay(500); + return; + } + stateTreeViewer.refreshJsonWithDelay(500); + + } + + public void loadImage() { + + showStateTreeJson(); + if (this.display==null) { + this.display=new ImageDisplay(); + } + display.refresh(); + display.setVisible(true); + } + public boolean isTrace() { return traceMode; } @@ -86,7 +199,25 @@ public boolean isInitialized() { public void setParsingConf(ParsingConf conf) { persistentParsingConf = conf; } - + + // move to a specified state using the state path stored (which represents the first route taken to reach the state) + public boolean moveToState(int identifier) { + if (identifier > stateGraph.size()) { + return false; + } + else { + List targetpath = new ArrayList<>(); + StateNode targetnode = stateGraph.getNodeById(identifier); + for (int i : targetnode.getPath()) { + targetpath.add(stateGraph.getNodeById(i)); + } + statePath.setPath(targetpath); + printGraph(); + loadImage(); + return true; + } + } + /** * initialize is a wrapper for initializing a model or trace which cleans up internal state if * initialization fails. @@ -94,7 +225,8 @@ public void setParsingConf(ParsingConf conf) { */ public boolean initialize(File file, boolean isTrace) { ParsingConf oldEmbeddedParsingConf = embeddedParsingConf; - + + // Ensure any embedded ParsingConf from a previously loaded model is removed. embeddedParsingConf = null; @@ -103,9 +235,19 @@ public boolean initialize(File file, boolean isTrace) { // The embedded conf of the new model shouldn't persist if load fails. embeddedParsingConf = oldEmbeddedParsingConf; } + if (res) { + printGraph(); + loadImage(); + savePath(); + } return res; } - + + + // replace the '/'s in dash states and transitions with '_' + public String formatString(String s) { + return s.replace('/', '_'); + } /** * performReverseStep goes backward by `steps` states in the current state traversal path. * @param steps @@ -122,7 +264,7 @@ public void performReverseStep(int steps) { statePath.decrementPosition(steps + 1, traceMode); performStep(1); } - + // If the user was on some alternate path, we need to perform `alt` until we get back // to the correct StateNode. while (!statePath.getCurNode().equals(targetNode)) { @@ -131,6 +273,9 @@ public void performReverseStep(int steps) { // Ensure the ID is set when reverse-stepping back to an alternative initial state. statePath.getCurNode().setIdentifier(targetNode.getIdentifier()); + //statePath.printPath(); + printGraph(); + loadImage(); } /** @@ -158,9 +303,10 @@ public boolean performStep(int steps, List constraints) { statePath.incrementPosition(steps); return true; } - + statePath.commitNodes(); - + + String pathPredicate = AlloyUtils.getPathPredicate(constraints, stateSigData); try { String curInitString; @@ -213,7 +359,11 @@ public boolean performStep(int steps, List constraints) { this.activeSolutions.clear(); this.activeSolutions.push(sol); - + //statePath.printPath(); + + printGraph(); + loadImage(); + savePath(); return true; } @@ -254,7 +404,11 @@ public boolean selectAlternatePath(boolean reverse) { } stateGraph.addNodes(startNode, stateNodes); - + //statePath.printPath(); + + printGraph(); + loadImage(); + savePath(); return true; } @@ -266,7 +420,7 @@ public boolean selectAlternatePath(boolean reverse) { */ public boolean performUntil(int limit) { String breakPredicate = AlloyUtils.getBreakPredicate(constraintManager.getConstraints(), stateSigData); - + for (int steps = 1; steps <= limit; steps++) { try { String curInitString; @@ -314,10 +468,11 @@ public boolean performUntil(int limit) { this.activeSolutions.clear(); this.activeSolutions.push(sol); - + printGraph(); + loadImage(); + savePath(); return true; } - return false; } @@ -370,7 +525,8 @@ public boolean setToInit() { activeSolutions.clear(); activeSolutions.push(sol); - + printGraph(); + loadImage(); return true; } @@ -384,6 +540,7 @@ public boolean setToInit() { public boolean validateConstraint(String constraint) { String breakPredicate = AlloyUtils.getBreakPredicate(Arrays.asList(constraint), stateSigData); + try { AlloyUtils.writeToFile( alloyModelString + alloyInitString + breakPredicate, @@ -417,7 +574,14 @@ public Map> getScopes() { public List getScopeForSig(String sigName) { return scopes.get(sigName); } - + + public String getStateString(int id) { + if (id<=0 || id-1>stateGraph.size()) { + return "state not found!"; + } + return stateGraph.getNode(id-1).toString(); + } + public String getCurrentStateString() { return statePath.getCurNode().toString(); } @@ -479,7 +643,7 @@ private boolean initializeWithModel(File model) { System.out.println("error. I/O failed."); return false; } - + alloyModelFile = tempModelFile; String modelString; @@ -588,7 +752,8 @@ private boolean initializeWithModel(File model) { System.out.printf("error. Sig %s not found.\n", getParsingConf().getStateSigName()); return false; } - + //System.out.println(getParsingConf().getStateSigName()); + stateSigData = new SigData(stateSig); List initialNodes = getStateNodesForA4Solution(sol); diff --git a/src/simulation/readme.md b/src/simulation/readme.md new file mode 100644 index 0000000..2cca0a7 --- /dev/null +++ b/src/simulation/readme.md @@ -0,0 +1,21 @@ +# Simulation Package README + +## Overview + +This package contains files that implement simulation within aldb. + +## Contents + +### 1. `Constaint/Alias Manager.java` +- **Purpose:** + - Contains functions for managing and validating constraints/aliases used by the break command. + +### 2. `GraphPrinter.java` +- **Purpose:** + - Runs graphviz commands in console to generate .png files or .json files for visualization. + +### 3. `SimulationManager.java` +- **Purpose:** + - Contains functions for simulation activities. Stores statePath and stateGraph that represent an alloy trace. Interacts with the alloy solver to take steps/alt/reverse, etc. + +- diff --git a/src/state/StateGraph.java b/src/state/StateGraph.java index 8ab3b51..885fdc0 100644 --- a/src/state/StateGraph.java +++ b/src/state/StateGraph.java @@ -12,7 +12,28 @@ public class StateGraph { public StateGraph() { nodes = new ArrayList<>(); } - + + public StateNode getNode(int i){ + return nodes.get(i); + } + public StateNode getNodeById(int identifier){ + for (StateNode i:nodes) { + if (i.getIdentifier()==identifier) { + return i; + } + } + return null; + } + + + + + + public void printGraph() { + for (StateNode i:nodes) { + System.out.println(i.getStateString()); + } + } /** * initWithNodes initializes the graph with initial nodes. * @param List nodes diff --git a/src/state/StateNode.java b/src/state/StateNode.java index a94272a..db335e9 100644 --- a/src/state/StateNode.java +++ b/src/state/StateNode.java @@ -9,28 +9,62 @@ import java.util.List; import java.util.SortedMap; import java.util.TreeMap; - +import ca.uwaterloo.watform.core.DashStrings; /** * StateNode represents a single execution state of an Alloy transition system. */ public class StateNode { private List steps; // outgoing edges (states that can be stepped to from this state) private SortedMap> state; // the state that this node represents + // can aldb support multi arity relations ?? + private int id; private ParsingConf parsingConf; private SigData sigData; + private List path; // redo with List public StateNode(SigData data, ParsingConf conf) { + //System.out.println("New state node created "); sigData = data; parsingConf = conf; steps = new ArrayList<>(); state = new TreeMap<>(); - + path = new ArrayList<>(); for (String field : sigData.getFields()) { + //System.out.println(field); state.put(field, new ArrayList<>()); } } - + //implement a function for look up in state map + + + + public boolean hasStable() { + if (state.get(DashStrings.stableName)!=null) { //refer to strings in dash core + return true; + } + return false; + } + + public boolean getStable() { + if (state.get("dsh_stable")!=null && state.get(DashStrings.stableName).contains(DashStrings.trueName)) { + return true; + } + return false; + } + + public void printId() { + System.out.println(id); + } + + public String getTransitionName(){ + return String.join(", ", state.get(DashStrings.transTakenName+"0")); + } + + public List getControlStateNames(){ + return state.get(DashStrings.confName+"0"); + } + public void addValueToField(String field, String value) { if (!state.containsKey(field)) { return; @@ -51,12 +85,22 @@ public void addValueToField(String field, String value) { valuesForField.add(value); } + + public void storePath(List input_path) { + path=input_path; + } + + public List getPath() { + return path; + } public List getSteps() { return steps; } public void addStep(StateNode node) { + //System.out.println("Adding new node to step:"); + //node.printId(); steps.add(node); } @@ -127,6 +171,7 @@ public String getAlloyInitString() { StringBuilder alloyFormattedValsBuilder = new StringBuilder(); String prefix = ""; for (String val : vals) { + //System.out.println(val); alloyFormattedValsBuilder.append(prefix); prefix = String.format(" %s ", AlloyConstants.PLUS); String[] values = val.split(AlloyConstants.SET_DELIMITER); @@ -159,14 +204,26 @@ public int getIdentifier() { public void setIdentifier(int id) { this.id = id; } - - private String getStateString() { + + public void printState() { + for (String key : state.keySet()) { + System.out.println(key); + System.out.println(state.get(key)); + } + } + + public String getStateString() { StringBuilder sb = new StringBuilder(); + //System.out.println("calling getstatestring function"); + //printState(); for (String key : state.keySet()) { + //System.out.println(key); sb.append(String.format("\n%s: %s ", key, AlloyConstants.BLOCK_INITIALIZER)); + //System.out.println(sb.toString()); sb.append(String.format("%s %s", String.join(", ", state.get(key)), AlloyConstants.BLOCK_TERMINATOR)); } sb.append("\n"); + return sb.toString(); } diff --git a/src/state/StatePath.java b/src/state/StatePath.java index 0f9f703..3c86f9a 100644 --- a/src/state/StatePath.java +++ b/src/state/StatePath.java @@ -16,7 +16,28 @@ public StatePath() { position = 0; tempPathSize = 0; } + + public void printPath() { + System.out.println("printing path"); + for (int i = 0; i < path.size(); i++) { + path.get(i).printId(); + } + } + public List getPath(){ + List result = new ArrayList<>(); + for (int i = 0; i < path.size(); i++) { + result.add(path.get(i).getIdentifier()); + } + return result; + } + public int getLength() { + return path.size(); + } + public int getIndex(StateNode target) { + return path.indexOf(target); + } + private void appendPath(List path) { this.path.addAll(path); position = this.path.size() - 1; @@ -93,10 +114,14 @@ public void clearPath() { path.clear(); tempPathSize = 0; } - + public void setPath(List Path) { + clearPath(); + appendPath(Path); + + } public String getHistory(int n, boolean traceMode) { int i = position - 1; - int j = i; + int j = i+1; int pos; StringBuilder sb = new StringBuilder(); while (j >= 0 && i - j < n) { diff --git a/src/state/readme.md b/src/state/readme.md new file mode 100644 index 0000000..d9e57b0 --- /dev/null +++ b/src/state/readme.md @@ -0,0 +1,21 @@ +# State Package README + +## Overview + +This package contains StateGraph, StatePath, StateNode objects that together stores and describes the states within a trace. + +## Contents + +### 1. `StateNode.java` +- **Purpose:** + - This class defines the structure of a StateNode. A StateNode stores its state information in a map and the StateNodes it can reach within one outgoing edge in a list of StateNodes + +### 2. `StatePath.java` +- **Purpose:** + - This class defines the structure of a StatePath. A StatePath is a list of StateNodes in the current path taken. + + +### 3. `StateGraph.java` +- **Purpose:** + - This class defines the structure of a StateGraph. A StateGraph is a list of all StateNodes visited. + \ No newline at end of file