Merge code for visualization, bug fix and extending aldb features

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)

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<String> rawConstraints, SigData sigData) {
         List<String> constraints = new ArrayList<String>();
+
         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<String> 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<String> 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.

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";

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.

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;

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;

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 {

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"};
+
+
 }
+

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;
+	                }
+	            }
             }
         }
 

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;

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;