diff --git a/.github/workflows/unit_tests.yml b/.github/workflows/unit_tests.yml new file mode 100644 index 0000000..08096de --- /dev/null +++ b/.github/workflows/unit_tests.yml @@ -0,0 +1,14 @@ +name: CI + +on: [push] + +jobs: + unit-tests: + + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v1 + - name: Unit tests + run: ant test + diff --git a/.gitignore b/.gitignore index a1c2a23..26bb8d1 100644 --- a/.gitignore +++ b/.gitignore @@ -11,7 +11,6 @@ .mtj.tmp/ # Package Files # -*.jar *.war *.nar *.ear @@ -21,3 +20,12 @@ # virtual machine crash logs, see http://www.java.com/en/download/help/error_hotspot.xml hs_err_pid* + +# IntelliJ IDEA files +.idea/ + +# Output directory for generated class files +bin/ + +# Output directory for distribution +dist/ diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..d2fc696 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,32 @@ +# Contributing + +Prior to submitting a PR, please ensure that: + +1. The proposed change has been clearly documented and motivated in a GitHub issue and discussed with the owners of this repository. +2. There is no existing or obsolete ticket which addresses your proposed change. + +## Build Requirements + +* Java 8 or later +* [Ant](https://ant.apache.org/) 1.10.7 or later + +## Build and Run + + $ ant + $ java -jar dist/aldb.jar + +## Running Tests + + $ ant test + +## Pull Request Process + +1. Ensure your code builds successfully. +2. Test your changes manually if possible by running the JAR and manipulating a non-trivial model if applicable. +3. Ensure that existing tests pass. +4. Ensure that you have added new tests where necessary. +5. Write a descriptive and concise commit message, PR title, and description. +6. Ensure that a GitHub issue is referenced in the PR description with a `Closes` statement. +7. Create your PR. +8. Once all status checks pass, assign one or more owners as reviewers. +9. Once you have at least one approval from an owner, you can squash and merge your PR. diff --git a/README.md b/README.md index 4bb2bd1..47ab450 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,391 @@ -# aldb-new -A debugger for transition systems modelled in Alloy +# ALDB + +## Introduction + +Alloy Debugger (ALDB) is a command-line debugger for transition systems modelled in Alloy. Transition systems are composed of some state that changes based on a transition relation. + +ALDB allows for incremental state-space exploration of Alloy transition systems, with the aim of reducing the time taken to validate and/or find bugs in a model. It can also incrementally explore XML counterexamples that are generated by the Alloy Analyzer. + +This guide explains usage of ALDB, compatibility requirements for Alloy models, and troubleshooting. It also includes an illustrative example of stepping through a concrete transition system using ALDB. + +### Table of Contents + +* [Getting Started](#getting-started) +* [Model and Configuration Format](#model-and-configuration-format) +* [Commands](#commands) +* [Usage Example](#usage-example) +* [Trace Mode](#trace-mode) +* [Session Recovery](#session-recovery) +* [Troubleshooting](#troubleshooting) +* [Reporting Issues](#reporting-issues) +* [Contributing](#contributing) +* [Contact](#contact) + +## 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). + +2. Run ALDB from the command line: + ```sh + $ java -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. + +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 `setconf` command. +When using the `setconf` command, the configuration will last for the entire ALDB session. + +The default configuration looks like the following: + +```yml +stateSigName: State +transitionRelationName: next +initPredicateName: init +additionalSigScopes: {} +``` + +`stateSigName` is the name of the signature that represents the changing state that the transition system tracks. + +`transitionRelationName` is the name of the transition relation that changes the state. + +`initPredicateName` is the name of the predicate that defines the initial state of the transition system. + +`additionalSigScopes` is a map of (String, Integer) pairs that define specific scopes for other signatures within the model. + +The Alloy code that conforms to the above configuration – with the configuration given in a comment block with the required header and footer – looks like the following: + +```Alloy +/* BEGIN_ALDB_CONF + * + * stateSigName: State + * transitionConstraintName: next + * initPredicateName: init + * + * END_ALDB_CONF + */ + +sig State { … } +pred init[s: 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. + +## Commands + +### Summary + +Command | Description +-- | -- +alt | Select an alternate execution path +break | Control the set of constraints used +current | Display the current state +dot | Dump DOT graph to disk +help | Display the list of available commands +history | Display past states +load | Load an Alloy model +quit | Exit ALDB +reverse-step | Go back n steps in the current state traversal path +scope | Display scope set +setconf | Set parsing options for an Alloy model +step | Perform a state transition of n steps +trace | Load a saved Alloy XML instance +until | Run until constraints are met + +### Detailed Descriptions + +#### alt +The `alt [-r]` command switches between alternative execution paths in the current trace. Multiple unique states can be reached for a given path length; this command allows the user to explore all those states. + +Specify the `-r` option to go back to the previous execution state. + +![image](https://user-images.githubusercontent.com/13455356/79278612-08626f00-7e7a-11ea-98b8-f8e59e8d12f5.png) + +#### break +The `break [-c] [-l] [-rm] ` command allows for specifying an execution constraint (breakpoint). Use these constraints to control certain parameters and invariants throughout the model’s execution. When stepping through the model, execution will halt if and when the constraint is satisfied. Running the command multiple times will result in a super-constraint composed of a disjunction of each individually-specified constraint. + +Specify the `-c` option to clear all constraints. +Specify the `-l` option to list all current constraints. +Specify the `-rm` option to remove a constraint. + +#### current +The `current [property]` command displays the values of all properties at the present execution state. + +Specify a specific property to view only its values. + +#### dot +The `dot` command writes the DOT graph representation of the states visited in the active model to a new file in the current working directory. + +#### help +The `help [cmd]` command lists available commands to use in ALDB, along with descriptions of what they do. + +Specify a cmd to view full documentation for that specific command. + +#### history +The `history [n]` command displays the past n consecutive states of the current execution path. + +Specify an integer value of n >= 1. By default, n = 3. + +![image](https://user-images.githubusercontent.com/13455356/77835857-59a6fa80-7127-11ea-8ba4-79563a279c47.png) + +#### load +The `load ` command loads and initializes the Alloy model specified by into ALDB. It will check for a {BEGIN | END}_ALDB_CONF comment block in to set the configuration, and then initialize the state graph to the initial state specified by the equivalent `init` predicate in the model. + +#### quit +The `quit` command exits ALDB. + +#### reverse-step +The `reverse-step [n]` command goes back by n steps in the current execution path. If n is larger than the current path length, this command takes the execution back to the initial state. + +Specify an integer value of n >= 1. By default, n = 1. + +![image](https://user-images.githubusercontent.com/13455356/77835867-793e2300-7127-11ea-9b10-bd670fe75a2b.png) +#### scope +The `scope [sig-name]` command displays the scope set for all signatures in the active model. + +Specify a sig-name to view the scope only for that specific signature. + +#### setconf +The `setconf [filename]` command sets custom parsing options for the current session. The file must be specified in YAML. The following properties are set by default: + +```yml +stateSigName: State +initPredicateName: init +transitionConstraintName: next +additionalSigScopes: {} +``` + +`stateSigName` is the name of the signature in the model that represents the state as it changes throughout the transition system’s execution. + +`initPredicateName` is the name of the predicate that initializes the first state. + +`transitionConstraintName` is the name of the transition function that alters the state. + +`additionalSigScopes` allows for specifying the cardinalities of signatures that are used during execution of the transition system. + +Running `setconf` with no filename will set the above default options. + +#### step +The `step [n]` command performs n state transitions from the current execution state, ending at one of the valid states for a length (current + n) state traversal from the initial state. + +Specify an integer value of n >= 1. By default, n = 1. + +![image](https://user-images.githubusercontent.com/13455356/79278678-347df000-7e7a-11ea-90d7-111733a448a6.png) + +#### trace +The `trace ` command loads a saved Alloy XML trace generated by the Alloy Analyzer. + +Specify the file to load from as `filename`. The contents must be in the Alloy XML format. + +#### until +The `until [limit]` command will run several forward steps of the transition system until it meets user-specified constraints. See the `break` command documentation for information about how to specify multiple constraints. + +Specify the `limit` in order to constrain the search space. In other words, ALDB will only check up to `limit` state transitions, and if the constraints have not been satisfied by then, it will not check any further transitions. `limit` must be an integer >= 1. By default, limit = 10. + +![image](https://user-images.githubusercontent.com/13455356/77835884-9a067880-7127-11ea-8808-16b692ee3ebe.png) + +## Usage Example + +This section will walk through solving the classic River Crossing Problem (RCP) via specification with Alloy and ALDB. + +In the RCP, there is a river dividing two sides of land. There is one boat, and it can carry a human and one other item or animal. A farmer, his fox, chicken, and a bag of grain are all on the near side of the river. The farmer must transport everything to the far side. There are some stipulations: + +- If the fox and chicken are on the same side without the farmer, then the fox eats the chicken. +- If the chicken and grain are on the same side without the farmer, then the chicken eats the grain. + +Solving the RCP entails finding a sequence of events that allows everything to be safely transported to the far side of the river. The following is an Alloy model representing the problem: + +```Alloy +/* Farmer and his possessions are objects. */ +abstract sig Object { eats: set Object } +one sig Farmer, Fox, Chicken, Grain extends Object {} + +/* Defines what eats what when the farmer is not around. */ +fact { eats = Fox->Chicken + Chicken->Grain } + +/* Stores the objects at the near and far sides of the river. */ +sig State { near, far: set Object } + +/* In the initial state, all objects are on the near side. */ +pred init [s: State] { + s.near = Object && no s.far +} + +/* At most one item to move from ‘from’ to ‘to’. */ +pred crossRiver [from, from’, to, to’: set Object] { + one x: from | { + from’ = from - x - Farmer - from’.eats + to’ = to + x + Farmer + } +} + +/* Transition to the next state. */ +pred next [s, s’: State] { + Farmer in s.near => + crossRiver [s.near, s’.near, s.far, s’.far] + else + 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) + +The changing state in the above model is the set of objects that are on the near and far sides. Initially, nothing is on the far side. The river can only be crossed starting from where the farmer currently is, and ending on the opposite side. When crossing the river, the farmer has the option to take any one of the other objects with them, with the consequence of something on that side potentially being eaten when left unattended. + +The goal is to use ALDB to find a set of state transitions that allows all objects to eventually safely reach the far side of the river. + +Begin by loading the model into ALDB. There is no need for a configuration here because the model as written conforms to the default names that ALDB uses for states and transition functions: State, init, next. + +``` +(aldb) load models/river_crossing.als +Reading model from models/river_crossing.als...done. +(aldb) current + +far: { } +near: { Chicken, Farmer, Fox, Grain } +``` + +The initial state is set as expected. Since the desired end state is known, using the until command with a breakpoint is the quickest method to get there. The breakpoint will be set by constraining the fair side to contain all the objects, and having nothing on the near side, as follows: + +``` +(aldb) break "far = Object && no near" +(aldb) until + +far: { Chicken, Farmer, Fox, Grain } +near: { } +``` + +Observe that the desired state has been reached. Use the history command to show the sequence of state transitions that got the execution to this point. + +``` +(aldb) history 10 + +(-7) +---- +far: { } +near: { Chicken, Farmer, Fox, Grain } + +(-6) +---- +far: { Chicken, Farmer } +near: { Fox, Grain } + +(-5) +---- +far: { Chicken } +near: { Farmer, Fox, Grain } + +(-4) +---- +far: { Chicken, Farmer, Fox } +near: { Grain } + +(-3) +---- +far: { Fox } +near: { Chicken, Farmer, Grain } + +(-2) +---- +far: { Farmer, Fox, Grain } +near: { Chicken } + +(-1) +---- +far: { Fox, Grain } +near: { Chicken, Farmer } +``` + +Now it is known that after seven transitions corresponding to the above, the desired end state can be reached. + +Alternatively, ALDB can incrementally explore the model’s state space by stepping. + +``` +(aldb) load models/river_crossing.als +Reading model from models/river_crossing.als...done. +(aldb) current + +far: { } +near: { Chicken, Farmer, Fox, Grain } + +(aldb) step + +far: { Farmer, Grain } +near: { Fox } +``` + +Observe that the reached state does not contain all the objects. The chicken is missing because in this specific execution path, the farmer took the grain and left the fox to eat the chicken. This behaviour is undesired, so the alt command can be used to explore other states that could have been reached with the same path length. + +``` +(aldb) step + +far: { Farmer, Grain } +near: { Fox } + +(aldb) alt + +far: { Farmer, Fox } +near: { Chicken } + +(aldb) alt + +far: { Chicken, Farmer } +near: { Fox, Grain } +``` + +In the first alternate state, the farmer took the fox, leaving the chicken to eat the grain. The second alternate state is the desired one. This process of manually exploring the state space exposes execution states that may not otherwise have been explored. Continue this process to eventually reach the desired end state, or to simply explore other intermediate states. + +## Trace Mode + +The Alloy Analyzer is able to generate counterexamples when inconsistencies are found during model checking. The counterexample is specified as an XML file, and then loaded into ALDB for exploration. + +Use the `trace ` command to load the counterexample into ALDB. There is no need to provide a configuration. Now it is possible to incrementally explore the counterexample states using the usual ALDB functions. + +Note that the original Alloy model from which the counterexample was generated need not be provided. If it is not, ALDB is unable to find alternate states or step beyond the final state of the counterexample. + +## Session Recovery + +Every unique execution of ALDB is considered to be a session. Each time ALDB is started, a session log is created under the directory referred to by `$TMPDIR`, with a naming scheme of: `aldb...
...`. This file records each full, completed command entered in the current session. + +If a session is terminated at any point, it can be recovered up to the point of the last completed command by starting ALDB with the `--restore` flag (`-r` shorthand) and the file path of the desired session log to restore from. A new session log with the contents of the previous session’s log (and any further commands) will be created for the new session. + +## Troubleshooting + +Error message | Solution +-- | -- +No such file. | Ensure that the file exists, and that the file path being provided is correct. +No file specified. | If the command requires a file, specify the file path after the command name. +Failed to read file. | The file exists but could not be read. Restart ALDB and try again. +Invalid configuration. | Ensure that the configuration is correctly specified in syntactically-valid YAML. +Invalid trace. | Ensure that the trace file is XML generated directly from the Alloy Analyzer. +Internal error. Failed to create temporary Alloy file. | Restart ALDB and try again. If this error continues to occur, restart the computer. +Undefined command. | The command does not exist. Ensure no typos. +Signature not found. | Ensure that the Sig being requested by the `scope` command exists in the model that was loaded. +No model file specified. | Use the `load` command to load an Alloy model, and then retry the action. +Session log could not be opened for reading. | Ensure that the given session log path is correct and the file exists. +Unable to create session log. | Restart ALDB and try again. If this error continues to occur, restart the computer. +Could not parse model. | Ensure that the model is written in valid Alloy code. Use the Alloy Analyzer to check. +Predicate not found. | Ensure that the predicate name specified in the configuration exists in the Alloy model. +Issue parsing predicate. | Ensure that the Alloy model is syntactically-valid. +I/O failed, cannot initialize model. | Restart ALDB and try again. If this error continues to occur, restart the computer. + +## Reporting Issues + +If you discover an issue, please report it by creating a GitHub issue. In the issue, please be descriptive and include as much of the following information as possible: + +1. ALDB version +2. Java version +3. OS version +4. Reproduction steps +5. Screenshots +6. Any other useful information + +## Contributing + +Please see [the contributing guidelines](CONTRIBUTING.md). + +## Contact + +For further discussion, questions, or anything else that may be unclear, please email nday@uwaterloo.ca. + diff --git a/build.xml b/build.xml new file mode 100644 index 0000000..ec43340 --- /dev/null +++ b/build.xml @@ -0,0 +1,97 @@ + + A debugger for transition systems modelled in Alloy. + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
+ + + +
+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/lib/argparse4j-0.8.1.jar b/lib/argparse4j-0.8.1.jar new file mode 100644 index 0000000..b3039f4 Binary files /dev/null and b/lib/argparse4j-0.8.1.jar differ diff --git a/lib/byte-buddy-1.10.5.jar b/lib/byte-buddy-1.10.5.jar new file mode 100644 index 0000000..88d950e Binary files /dev/null and b/lib/byte-buddy-1.10.5.jar differ diff --git a/lib/byte-buddy-agent-1.10.5.jar b/lib/byte-buddy-agent-1.10.5.jar new file mode 100644 index 0000000..f2b93b6 Binary files /dev/null and b/lib/byte-buddy-agent-1.10.5.jar differ diff --git a/lib/jline-3.9.0.jar b/lib/jline-3.9.0.jar new file mode 100644 index 0000000..753a0d0 Binary files /dev/null and b/lib/jline-3.9.0.jar differ diff --git a/lib/junit-platform-console-standalone-1.5.2.jar b/lib/junit-platform-console-standalone-1.5.2.jar new file mode 100755 index 0000000..76a2f91 Binary files /dev/null and b/lib/junit-platform-console-standalone-1.5.2.jar differ diff --git a/lib/mockito-core-3.3.2.jar b/lib/mockito-core-3.3.2.jar new file mode 100644 index 0000000..f04628a Binary files /dev/null and b/lib/mockito-core-3.3.2.jar differ diff --git a/lib/objenesis-2.6.jar b/lib/objenesis-2.6.jar new file mode 100644 index 0000000..b4b29d5 Binary files /dev/null and b/lib/objenesis-2.6.jar differ diff --git a/lib/one-jar-ant-task-0.97.jar b/lib/one-jar-ant-task-0.97.jar new file mode 100644 index 0000000..567ce75 Binary files /dev/null and b/lib/one-jar-ant-task-0.97.jar differ diff --git a/lib/org.alloytools.alloy.dist-5.1.0.jar b/lib/org.alloytools.alloy.dist-5.1.0.jar new file mode 100644 index 0000000..5720727 Binary files /dev/null and b/lib/org.alloytools.alloy.dist-5.1.0.jar differ diff --git a/lib/snakeyaml-1.25.jar b/lib/snakeyaml-1.25.jar new file mode 100644 index 0000000..0004985 Binary files /dev/null and b/lib/snakeyaml-1.25.jar differ diff --git a/lib/system-rules-1.19.0.jar b/lib/system-rules-1.19.0.jar new file mode 100644 index 0000000..9e333ad Binary files /dev/null and b/lib/system-rules-1.19.0.jar differ diff --git a/licenses/LICENSE-Alloy b/licenses/LICENSE-Alloy new file mode 100644 index 0000000..cf33d1b --- /dev/null +++ b/licenses/LICENSE-Alloy @@ -0,0 +1,204 @@ +# THIS IS NOT VALID YET! CURRENTLY CODE IS UNDER MIT LICENSE + + +Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "{}" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright {yyyy} {name of copyright owner} + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. \ No newline at end of file diff --git a/licenses/LICENSE-Argparse4j b/licenses/LICENSE-Argparse4j new file mode 100644 index 0000000..2354213 --- /dev/null +++ b/licenses/LICENSE-Argparse4j @@ -0,0 +1,23 @@ +/* + * Copyright (C) 2011-2017 Tatsuhiro Tsujikawa + * + * Permission is hereby granted, free of charge, to any person + * obtaining a copy of this software and associated documentation + * files (the "Software"), to deal in the Software without + * restriction, including without limitation the rights to use, copy, + * modify, merge, publish, distribute, sublicense, and/or sell copies + * of the Software, and to permit persons to whom the Software is + * furnished to do so, subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND + * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS + * BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN + * ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN + * CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + * SOFTWARE. + */ \ No newline at end of file diff --git a/licenses/LICENSE-JLine b/licenses/LICENSE-JLine new file mode 100644 index 0000000..d5a0599 --- /dev/null +++ b/licenses/LICENSE-JLine @@ -0,0 +1,34 @@ +Copyright (c) 2002-2016, the original author or authors. +All rights reserved. + +http://www.opensource.org/licenses/bsd-license.php + +Redistribution and use in source and binary forms, with or +without modification, are permitted provided that the following +conditions are met: + +Redistributions of source code must retain the above copyright +notice, this list of conditions and the following disclaimer. + +Redistributions in binary form must reproduce the above copyright +notice, this list of conditions and the following disclaimer +in the documentation and/or other materials provided with +the distribution. + +Neither the name of JLine nor the names of its contributors +may be used to endorse or promote products derived from this +software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, +BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY +AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO +EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE +FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, +OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED +AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT +LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING +IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED +OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/licenses/LICENSE-JUnit b/licenses/LICENSE-JUnit new file mode 100644 index 0000000..75658b3 --- /dev/null +++ b/licenses/LICENSE-JUnit @@ -0,0 +1,213 @@ +JUnit + +Eclipse Public License - v 1.0 + +THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS ECLIPSE PUBLIC +LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR DISTRIBUTION OF THE PROGRAM +CONSTITUTES RECIPIENT'S ACCEPTANCE OF THIS AGREEMENT. + +1. DEFINITIONS + +"Contribution" means: + + a) in the case of the initial Contributor, the initial code and + documentation distributed under this Agreement, and + b) in the case of each subsequent Contributor: + + i) changes to the Program, and + + ii) additions to the Program; + + where such changes and/or additions to the Program originate from and are +distributed by that particular Contributor. A Contribution 'originates' from a +Contributor if it was added to the Program by such Contributor itself or anyone +acting on such Contributor's behalf. Contributions do not include additions to +the Program which: (i) are separate modules of software distributed in +conjunction with the Program under their own license agreement, and (ii) are +not derivative works of the Program. + +"Contributor" means any person or entity that distributes the Program. + +"Licensed Patents " mean patent claims licensable by a Contributor which are +necessarily infringed by the use or sale of its Contribution alone or when +combined with the Program. + +"Program" means the Contributions distributed in accordance with this Agreement. + +"Recipient" means anyone who receives the Program under this Agreement, +including all Contributors. + +2. GRANT OF RIGHTS + + a) Subject to the terms of this Agreement, each Contributor hereby grants +Recipient a non-exclusive, worldwide, royalty-free copyright license to +reproduce, prepare derivative works of, publicly display, publicly perform, +distribute and sublicense the Contribution of such Contributor, if any, and +such derivative works, in source code and object code form. + + b) Subject to the terms of this Agreement, each Contributor hereby grants +Recipient a non-exclusive, worldwide, royalty-free patent license under +Licensed Patents to make, use, sell, offer to sell, import and otherwise +transfer the Contribution of such Contributor, if any, in source code and +object code form. This patent license shall apply to the combination of the +Contribution and the Program if, at the time the Contribution is added by the +Contributor, such addition of the Contribution causes such combination to be +covered by the Licensed Patents. The patent license shall not apply to any +other combinations which include the Contribution. No hardware per se is +licensed hereunder. + + c) Recipient understands that although each Contributor grants the +licenses to its Contributions set forth herein, no assurances are provided by +any Contributor that the Program does not infringe the patent or other +intellectual property rights of any other entity. Each Contributor disclaims +any liability to Recipient for claims brought by any other entity based on +infringement of intellectual property rights or otherwise. As a condition to +exercising the rights and licenses granted hereunder, each Recipient hereby +assumes sole responsibility to secure any other intellectual property rights +needed, if any. For example, if a third party patent license is required to +allow Recipient to distribute the Program, it is Recipient's responsibility to +acquire that license before distributing the Program. + + d) Each Contributor represents that to its knowledge it has sufficient +copyright rights in its Contribution, if any, to grant the copyright license +set forth in this Agreement. + +3. REQUIREMENTS + +A Contributor may choose to distribute the Program in object code form under +its own license agreement, provided that: + + a) it complies with the terms and conditions of this Agreement; and + + b) its license agreement: + + i) effectively disclaims on behalf of all Contributors all warranties and +conditions, express and implied, including warranties or conditions of title +and non-infringement, and implied warranties or conditions of merchantability +and fitness for a particular purpose; + + ii) effectively excludes on behalf of all Contributors all liability for +damages, including direct, indirect, special, incidental and consequential +damages, such as lost profits; + + iii) states that any provisions which differ from this Agreement are +offered by that Contributor alone and not by any other party; and + + iv) states that source code for the Program is available from such +Contributor, and informs licensees how to obtain it in a reasonable manner on +or through a medium customarily used for software exchange. + +When the Program is made available in source code form: + + a) it must be made available under this Agreement; and + + b) a copy of this Agreement must be included with each copy of the +Program. + +Contributors may not remove or alter any copyright notices contained within the +Program. + +Each Contributor must identify itself as the originator of its Contribution, if +any, in a manner that reasonably allows subsequent Recipients to identify the +originator of the Contribution. + +4. COMMERCIAL DISTRIBUTION + +Commercial distributors of software may accept certain responsibilities with +respect to end users, business partners and the like. While this license is +intended to facilitate the commercial use of the Program, the Contributor who +includes the Program in a commercial product offering should do so in a manner +which does not create potential liability for other Contributors. Therefore, if +a Contributor includes the Program in a commercial product offering, such +Contributor ("Commercial Contributor") hereby agrees to defend and indemnify +every other Contributor ("Indemnified Contributor") against any losses, damages +and costs (collectively "Losses") arising from claims, lawsuits and other legal +actions brought by a third party against the Indemnified Contributor to the +extent caused by the acts or omissions of such Commercial Contributor in +connection with its distribution of the Program in a commercial product +offering. The obligations in this section do not apply to any claims or Losses +relating to any actual or alleged intellectual property infringement. In order +to qualify, an Indemnified Contributor must: a) promptly notify the Commercial +Contributor in writing of such claim, and b) allow the Commercial Contributor +to control, and cooperate with the Commercial Contributor in, the defense and +any related settlement negotiations. The Indemnified Contributor may +participate in any such claim at its own expense. + +For example, a Contributor might include the Program in a commercial product +offering, Product X. That Contributor is then a Commercial Contributor. If that +Commercial Contributor then makes performance claims, or offers warranties +related to Product X, those performance claims and warranties are such +Commercial Contributor's responsibility alone. Under this section, the +Commercial Contributor would have to defend claims against the other +Contributors related to those performance claims and warranties, and if a court +requires any other Contributor to pay any damages as a result, the Commercial +Contributor must pay those damages. + +5. NO WARRANTY + +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, THE PROGRAM IS PROVIDED ON AN +"AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, EITHER EXPRESS OR +IMPLIED INCLUDING, WITHOUT LIMITATION, ANY WARRANTIES OR CONDITIONS OF TITLE, +NON-INFRINGEMENT, MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. Each +Recipient is solely responsible for determining the appropriateness of using +and distributing the Program and assumes all risks associated with its exercise +of rights under this Agreement, including but not limited to the risks and +costs of program errors, compliance with applicable laws, damage to or loss of +data, programs or equipment, and unavailability or interruption of operations. + +6. DISCLAIMER OF LIABILITY + +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, NEITHER RECIPIENT NOR ANY +CONTRIBUTORS SHALL HAVE ANY LIABILITY FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING WITHOUT LIMITATION LOST +PROFITS), HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY +WAY OUT OF THE USE OR DISTRIBUTION OF THE PROGRAM OR THE EXERCISE OF ANY RIGHTS +GRANTED HEREUNDER, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. + +7. GENERAL + +If any provision of this Agreement is invalid or unenforceable under applicable +law, it shall not affect the validity or enforceability of the remainder of the +terms of this Agreement, and without further action by the parties hereto, such +provision shall be reformed to the minimum extent necessary to make such +provision valid and enforceable. + +If Recipient institutes patent litigation against any +entity (including a cross-claim or counterclaim in a lawsuit) alleging that the +Program itself (excluding combinations of the Program with other software or +hardware) infringes such Recipient's patent(s), then such Recipient's rights +granted under Section 2(b) shall terminate as of the date such litigation is +filed. + +All Recipient's rights under this Agreement shall terminate if it fails to +comply with any of the material terms or conditions of this Agreement and does +not cure such failure in a reasonable period of time after becoming aware of +such noncompliance. If all Recipient's rights under this Agreement terminate, +Recipient agrees to cease use and distribution of the Program as soon as +reasonably practicable. However, Recipient's obligations under this Agreement +and any licenses granted by Recipient relating to the Program shall continue +and survive. + +Everyone is permitted to copy and distribute copies of this Agreement, but in +order to avoid inconsistency the Agreement is copyrighted and may only be +modified in the following manner. The Agreement Steward reserves the right to +publish new versions (including revisions) of this Agreement from time to time. +No one other than the Agreement Steward has the right to modify this Agreement. +The Eclipse Foundation is the initial Agreement Steward. The Eclipse Foundation may assign the responsibility to +serve as the Agreement Steward to a suitable separate entity. Each new version +of the Agreement will be given a distinguishing version number. The Program +(including Contributions) may always be distributed subject to the version of +the Agreement under which it was received. In addition, after a new version of +the Agreement is published, Contributor may elect to distribute the Program +(including its Contributions) under the new version. Except as expressly stated +in Sections 2(a) and 2(b) above, Recipient receives no rights or licenses to +the intellectual property of any Contributor under this Agreement, whether +expressly, by implication, estoppel or otherwise. All rights in the Program not +expressly granted under this Agreement are reserved. + +This Agreement is governed by the laws of the State of New York and the +intellectual property laws of the United States of America. No party to this +Agreement will bring a legal action under this Agreement more than one year +after the cause of action arose. Each party waives its rights to a jury trial +in any resulting litigation. diff --git a/licenses/LICENSE-Mockito b/licenses/LICENSE-Mockito new file mode 100644 index 0000000..5a311f7 --- /dev/null +++ b/licenses/LICENSE-Mockito @@ -0,0 +1,21 @@ +The MIT License + +Copyright (c) 2007 Mockito contributors + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. diff --git a/licenses/LICENSE-Objenesis b/licenses/LICENSE-Objenesis new file mode 100644 index 0000000..d645695 --- /dev/null +++ b/licenses/LICENSE-Objenesis @@ -0,0 +1,202 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/licenses/LICENSE-One-JAR b/licenses/LICENSE-One-JAR new file mode 100644 index 0000000..d88102c --- /dev/null +++ b/licenses/LICENSE-One-JAR @@ -0,0 +1,32 @@ +/* + * One-JAR™ (http://www.simontuffs.com/one-jar). Copyright (c) 2004-2010, + * P. Simon Tuffs (simon@simontuffs.com). All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * Redistributions of source code must retain the above copyright notice, this + * list of conditions and the following disclaimer. + * + * Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * + * Neither the name of P. Simon Tuffs, nor the names of any contributors, + * nor the name One-JAR may be used to endorse or promote products derived + * from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + * + * Including this file inside the built One-JAR file conforms with these terms. + */ diff --git a/licenses/LICENSE-SnakeYAML b/licenses/LICENSE-SnakeYAML new file mode 100644 index 0000000..d9a10c0 --- /dev/null +++ b/licenses/LICENSE-SnakeYAML @@ -0,0 +1,176 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS diff --git a/licenses/LICENSE-byte-buddy b/licenses/LICENSE-byte-buddy new file mode 100644 index 0000000..d0381d6 --- /dev/null +++ b/licenses/LICENSE-byte-buddy @@ -0,0 +1,176 @@ +Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS diff --git a/licenses/LICENSE-system-rules b/licenses/LICENSE-system-rules new file mode 100644 index 0000000..2b28bf4 --- /dev/null +++ b/licenses/LICENSE-system-rules @@ -0,0 +1,213 @@ +Common Public License Version 1.0 + +THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS COMMON PUBLIC +LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR DISTRIBUTION OF THE PROGRAM +CONSTITUTES RECIPIENT'S ACCEPTANCE OF THIS AGREEMENT. + +1. DEFINITIONS + +"Contribution" means: + +a) in the case of the initial Contributor, the initial code and +documentation distributed under this Agreement, and + +b) in the case of each subsequent Contributor: + +i) changes to the Program, and + +ii) additions to the Program; + +where such changes and/or additions to the Program originate from and are +distributed by that particular Contributor. A Contribution 'originates' from a +Contributor if it was added to the Program by such Contributor itself or anyone +acting on such Contributor's behalf. Contributions do not include additions to +the Program which: (i) are separate modules of software distributed in +conjunction with the Program under their own license agreement, and (ii) are not +derivative works of the Program. + +"Contributor" means any person or entity that distributes the Program. + +"Licensed Patents " mean patent claims licensable by a Contributor which are +necessarily infringed by the use or sale of its Contribution alone or when +combined with the Program. + +"Program" means the Contributions distributed in accordance with this Agreement. + +"Recipient" means anyone who receives the Program under this Agreement, +including all Contributors. + +2. GRANT OF RIGHTS + +a) Subject to the terms of this Agreement, each Contributor hereby grants +Recipient a non-exclusive, worldwide, royalty-free copyright license to +reproduce, prepare derivative works of, publicly display, publicly perform, +distribute and sublicense the Contribution of such Contributor, if any, and such +derivative works, in source code and object code form. + +b) Subject to the terms of this Agreement, each Contributor hereby grants +Recipient a non-exclusive, worldwide, royalty-free patent license under Licensed +Patents to make, use, sell, offer to sell, import and otherwise transfer the +Contribution of such Contributor, if any, in source code and object code form. +This patent license shall apply to the combination of the Contribution and the +Program if, at the time the Contribution is added by the Contributor, such +addition of the Contribution causes such combination to be covered by the +Licensed Patents. The patent license shall not apply to any other combinations +which include the Contribution. No hardware per se is licensed hereunder. + +c) Recipient understands that although each Contributor grants the licenses +to its Contributions set forth herein, no assurances are provided by any +Contributor that the Program does not infringe the patent or other intellectual +property rights of any other entity. Each Contributor disclaims any liability to +Recipient for claims brought by any other entity based on infringement of +intellectual property rights or otherwise. As a condition to exercising the +rights and licenses granted hereunder, each Recipient hereby assumes sole +responsibility to secure any other intellectual property rights needed, if any. +For example, if a third party patent license is required to allow Recipient to +distribute the Program, it is Recipient's responsibility to acquire that license +before distributing the Program. + +d) Each Contributor represents that to its knowledge it has sufficient +copyright rights in its Contribution, if any, to grant the copyright license set +forth in this Agreement. + +3. REQUIREMENTS + +A Contributor may choose to distribute the Program in object code form under its +own license agreement, provided that: + +a) it complies with the terms and conditions of this Agreement; and + +b) its license agreement: + +i) effectively disclaims on behalf of all Contributors all warranties and +conditions, express and implied, including warranties or conditions of title and +non-infringement, and implied warranties or conditions of merchantability and +fitness for a particular purpose; + +ii) effectively excludes on behalf of all Contributors all liability for +damages, including direct, indirect, special, incidental and consequential +damages, such as lost profits; + +iii) states that any provisions which differ from this Agreement are offered +by that Contributor alone and not by any other party; and + +iv) states that source code for the Program is available from such +Contributor, and informs licensees how to obtain it in a reasonable manner on or +through a medium customarily used for software exchange. + +When the Program is made available in source code form: + +a) it must be made available under this Agreement; and + +b) a copy of this Agreement must be included with each copy of the Program. + +Contributors may not remove or alter any copyright notices contained within the +Program. + +Each Contributor must identify itself as the originator of its Contribution, if +any, in a manner that reasonably allows subsequent Recipients to identify the +originator of the Contribution. + +4. COMMERCIAL DISTRIBUTION + +Commercial distributors of software may accept certain responsibilities with +respect to end users, business partners and the like. While this license is +intended to facilitate the commercial use of the Program, the Contributor who +includes the Program in a commercial product offering should do so in a manner +which does not create potential liability for other Contributors. Therefore, if +a Contributor includes the Program in a commercial product offering, such +Contributor ("Commercial Contributor") hereby agrees to defend and indemnify +every other Contributor ("Indemnified Contributor") against any losses, damages +and costs (collectively "Losses") arising from claims, lawsuits and other legal +actions brought by a third party against the Indemnified Contributor to the +extent caused by the acts or omissions of such Commercial Contributor in +connection with its distribution of the Program in a commercial product +offering. The obligations in this section do not apply to any claims or Losses +relating to any actual or alleged intellectual property infringement. In order +to qualify, an Indemnified Contributor must: a) promptly notify the Commercial +Contributor in writing of such claim, and b) allow the Commercial Contributor to +control, and cooperate with the Commercial Contributor in, the defense and any +related settlement negotiations. The Indemnified Contributor may participate in +any such claim at its own expense. + +For example, a Contributor might include the Program in a commercial product +offering, Product X. That Contributor is then a Commercial Contributor. If that +Commercial Contributor then makes performance claims, or offers warranties +related to Product X, those performance claims and warranties are such +Commercial Contributor's responsibility alone. Under this section, the +Commercial Contributor would have to defend claims against the other +Contributors related to those performance claims and warranties, and if a court +requires any other Contributor to pay any damages as a result, the Commercial +Contributor must pay those damages. + +5. NO WARRANTY + +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, THE PROGRAM IS PROVIDED ON AN +"AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, EITHER EXPRESS OR +IMPLIED INCLUDING, WITHOUT LIMITATION, ANY WARRANTIES OR CONDITIONS OF TITLE, +NON-INFRINGEMENT, MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE. Each +Recipient is solely responsible for determining the appropriateness of using and +distributing the Program and assumes all risks associated with its exercise of +rights under this Agreement, including but not limited to the risks and costs of +program errors, compliance with applicable laws, damage to or loss of data, +programs or equipment, and unavailability or interruption of operations. + +6. DISCLAIMER OF LIABILITY + +EXCEPT AS EXPRESSLY SET FORTH IN THIS AGREEMENT, NEITHER RECIPIENT NOR ANY +CONTRIBUTORS SHALL HAVE ANY LIABILITY FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING WITHOUT LIMITATION LOST +PROFITS), HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, +STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY +OUT OF THE USE OR DISTRIBUTION OF THE PROGRAM OR THE EXERCISE OF ANY RIGHTS +GRANTED HEREUNDER, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGES. + +7. GENERAL + +If any provision of this Agreement is invalid or unenforceable under applicable +law, it shall not affect the validity or enforceability of the remainder of the +terms of this Agreement, and without further action by the parties hereto, such +provision shall be reformed to the minimum extent necessary to make such +provision valid and enforceable. + +If Recipient institutes patent litigation against a Contributor with respect to +a patent applicable to software (including a cross-claim or counterclaim in a +lawsuit), then any patent licenses granted by that Contributor to such Recipient +under this Agreement shall terminate as of the date such litigation is filed. In +addition, if Recipient institutes patent litigation against any entity +(including a cross-claim or counterclaim in a lawsuit) alleging that the Program +itself (excluding combinations of the Program with other software or hardware) +infringes such Recipient's patent(s), then such Recipient's rights granted under +Section 2(b) shall terminate as of the date such litigation is filed. + +All Recipient's rights under this Agreement shall terminate if it fails to +comply with any of the material terms or conditions of this Agreement and does +not cure such failure in a reasonable period of time after becoming aware of +such noncompliance. If all Recipient's rights under this Agreement terminate, +Recipient agrees to cease use and distribution of the Program as soon as +reasonably practicable. However, Recipient's obligations under this Agreement +and any licenses granted by Recipient relating to the Program shall continue and +survive. + +Everyone is permitted to copy and distribute copies of this Agreement, but in +order to avoid inconsistency the Agreement is copyrighted and may only be +modified in the following manner. The Agreement Steward reserves the right to +publish new versions (including revisions) of this Agreement from time to time. +No one other than the Agreement Steward has the right to modify this Agreement. +IBM is the initial Agreement Steward. IBM may assign the responsibility to serve +as the Agreement Steward to a suitable separate entity. Each new version of the +Agreement will be given a distinguishing version number. The Program (including +Contributions) may always be distributed subject to the version of the Agreement +under which it was received. In addition, after a new version of the Agreement +is published, Contributor may elect to distribute the Program (including its +Contributions) under the new version. Except as expressly stated in Sections +2(a) and 2(b) above, Recipient receives no rights or licenses to the +intellectual property of any Contributor under this Agreement, whether +expressly, by implication, estoppel or otherwise. All rights in the Program not +expressly granted under this Agreement are reserved. + +This Agreement is governed by the laws of the State of New York and the +intellectual property laws of the United States of America. No party to this +Agreement will bring a legal action under this Agreement more than one year +after the cause of action arose. Each party waives its rights to a jury trial in +any resulting litigation. diff --git a/models/musical_chairs.als b/models/musical_chairs.als new file mode 100644 index 0000000..70a486b --- /dev/null +++ b/models/musical_chairs.als @@ -0,0 +1,134 @@ +/* Authors: Sabria Farheen, Nancy A. Day, Amirhossein Vakili, Ali Abbassi + * Date: October 1, 2017 + */ + +/* BEGIN_ALDB_CONF + * + * # Name of the transition relation in the Alloy model. + * transitionRelationName: trans + * + * # Additional Alloy sig scopes to specify. + * additionalSigScopes: + * Chair: 3 + * Player: 4 + * + * END_ALDB_CONF + */ + +open util/integer + +//***********************STATE SPACE*************************// +sig Chair, Player {} +abstract sig Mode {} +one sig start, walking, sitting, end extends Mode {} + +sig State { + // current players + players: set Player, + //current chairs + chairs: set Chair, + // current chair player relation + occupied: set Chair -> set Player, + // current state of game, should always be 1 + mode : set Mode +} + +//*****************INITIAL STATE CONSTRAINTS********************// + +pred init [s:State] { + s.mode = start + #s.players > 1 + #s.players = (#s.chairs).plus[1] + // force all Chair and Player to be included + s.players = Player + s.chairs = Chair + s.occupied = none -> none +} + +//**********************TRANSITION CONSTRAINTS***********************// +pred pre_music_starts [s: State] { + #s.players > 1 + s.mode = start +} +pred post_music_starts [s, s': State] { + s'.players = s.players + s'.chairs = s.chairs + // no one is sitting after music starts + s'.occupied = none -> none + s'.mode= walking +} +pred music_starts [s, s': State] { + pre_music_starts[s] + post_music_starts[s,s'] +} + +pred pre_music_stops [s: State] { + s.mode = walking +} +pred post_music_stops [s, s': State] { + s'.players = s.players + s'.chairs = s.chairs + // no other chair/player than chairs/players + s'.occupied in s'.chairs -> s'.players + // forcing occupied to be total and + //each chair mapped to only one player + all c:s'.chairs | one c.(s'.occupied) + // each "occupying" player is sitting on one chair + all p:Chair.(s'.occupied) | one s'.occupied.p + s'.mode = sitting +} +pred music_stops [s, s': State] { + pre_music_stops[s] + post_music_stops[s,s'] +} + +pred pre_eliminate_loser [s: State] { + s.mode = sitting +} +pred post_eliminate_loser [s, s': State] { + // loser is the player in the game not in the range of occupied + s'.players = Chair.(s.occupied) + #s'.chairs = (#s.chairs).minus[1] + s'.mode = start +} +pred eliminate_loser [s, s': State] { + pre_eliminate_loser[s] + post_eliminate_loser[s,s'] +} + +pred pre_declare_winner [s: State] { + #s.players = 1 + s.mode = start +} +pred post_declare_winner [s, s': State] { + s'.players = s.players + s'.chairs = s.chairs + s'.mode = end +} +pred declare_winner [s, s': State] { + pre_declare_winner[s] + post_declare_winner[s,s'] +} + +pred pre_end_loop [s: State] { + s.mode = end +} +pred post_end_loop [s, s': State] { + s'.mode = end + s'.players = s.players + s'.chairs = s.chairs + s'.occupied = s.occupied +} +pred end_loop [s, s': State] { + pre_end_loop[s] + post_end_loop[s,s'] +} + +// helper to define valid transitions +pred trans [s,s': State] { + music_starts[s,s'] or + music_stops[s,s'] or + eliminate_loser[s,s'] or + declare_winner[s,s'] or + end_loop[s,s'] +} diff --git a/models/river_crossing.als b/models/river_crossing.als new file mode 100644 index 0000000..8271f15 --- /dev/null +++ b/models/river_crossing.als @@ -0,0 +1,31 @@ +/* Adapted from the tutorial River Crossing Model: http://alloytools.org/tutorials/online/frame-RC-1.html */ + +/* Farmer and his possessions are objects. */ +abstract sig Object { eats: set Object } +one sig Farmer, Fox, Chicken, Grain extends Object {} + +/* Defines what eats what and the farmer is not around. */ +fact { eats = Fox->Chicken + Chicken->Grain} + +/* Stores the objects at near and far side of river. */ +sig State { near, far: set Object } + +/* In the initial state, all objects are on the near side. */ +pred init[s:State] { + s.near = Object && no s.far +} + +/* At most one item to move from 'from' to 'to' */ +pred crossRiver [from, from', to, to': set Object] { + one x: from | { + from' = from - x - Farmer - from'.eats + to' = to + x + Farmer + } +} + +pred next[s, s': State] { + Farmer in s.near => + crossRiver [s.near, s'.near, s.far, s'.far] + else + crossRiver [s.far, s'.far, s.near, s'.near] +} diff --git a/models/switch.als b/models/switch.als new file mode 100644 index 0000000..a47d59d --- /dev/null +++ b/models/switch.als @@ -0,0 +1,20 @@ +abstract sig Switch {} + +one sig On, Off extends Switch {} + +sig State { + a: Switch, + b: Switch +} + +pred init[s: State] { + s.a = On + s.b = Off +} + +pred next[s, s': State] { + s.a = On implies s'.a = Off + s.a = Off implies s'.a = On + s.b = On implies s'.b = Off + s.b = Off implies s'.b = On +} diff --git a/src/alloy/AlloyConstants.java b/src/alloy/AlloyConstants.java new file mode 100644 index 0000000..7f55933 --- /dev/null +++ b/src/alloy/AlloyConstants.java @@ -0,0 +1,20 @@ +package alloy; + +public class AlloyConstants { + public static final String ALLOY_ATOM_SEPARATOR = "\\$"; + public static final String BLOCK_INITIALIZER = "{"; + public static final String BLOCK_TERMINATOR = "}"; + public static final String NONE = "none"; + public static final String TRACE_SOURCE_TAG = "source"; + public static final String TRACE_FILENAME_ATTR = "filename"; + public static final String TRACE_CONTENT_ATTR = "content"; + public static final String PLUS = "+"; + public static final String UNDERSCORE = "_"; + public static final String SET_DELIMITER = "->"; + public static final String VALUE_SUFFIX = "$0"; + public static final String THIS = "this/"; + public static final String UNIV = "univ"; + public static final String CONCRETE_SIG_REGEX = "(.*)_(\\d+)"; + public static final String OR = "or"; + public static final String BREAK_PREDICATE_NAME = "break"; +} diff --git a/src/alloy/AlloyInterface.java b/src/alloy/AlloyInterface.java new file mode 100644 index 0000000..6441092 --- /dev/null +++ b/src/alloy/AlloyInterface.java @@ -0,0 +1,109 @@ +package alloy; + +import edu.mit.csail.sdg.alloy4.A4Reporter; +import edu.mit.csail.sdg.alloy4.Err; +import edu.mit.csail.sdg.alloy4.XMLNode; +import edu.mit.csail.sdg.ast.Command; +import edu.mit.csail.sdg.ast.Sig; +import edu.mit.csail.sdg.ast.Sig.Field; +import edu.mit.csail.sdg.parser.CompUtil; +import edu.mit.csail.sdg.parser.CompModule; +import edu.mit.csail.sdg.translator.A4Options; +import edu.mit.csail.sdg.translator.A4Solution; +import edu.mit.csail.sdg.translator.A4SolutionReader; +import edu.mit.csail.sdg.translator.A4TupleSet; +import edu.mit.csail.sdg.translator.TranslateAlloyToKodkod; + +import java.io.BufferedWriter; +import java.io.File; +import java.io.FileWriter; +import java.nio.file.Files; +import java.nio.file.Path; +import java.nio.file.Paths; +import java.util.ArrayList; +import java.util.List; + +public class AlloyInterface { + private static final A4Reporter reporter = new A4Reporter(); + private static final A4Options options = new A4Options(); + + public static CompModule compile(String modelPath) { + try { + return CompUtil.parseEverything_fromFile(reporter, null, modelPath); + } catch (Err e) {} + + return null; + } + + public static A4Solution run(CompModule module) { + List commands = module.getAllCommands(); + if (commands.isEmpty()) { + return null; + } + + // Use the command injected by us at the end of the input + // model. This ensures any extraneous commands in the input model are + // not run. + Command command = commands.get(commands.size() - 1); + return TranslateAlloyToKodkod.execute_command( + reporter, module.getAllReachableSigs(), command, options); + } + + /** + * solutionFromXMLFile reads an Alloy XML file and returns an A4Solution + * using the Alloy API. The root model and all included files are obtained + * from the XML file and saved to disk, as required by the API. + * @param File + * @return A4Solution + */ + public static A4Solution solutionFromXMLFile(File file) throws Exception { + Path tempDir = Files.createTempDirectory("aldb"); + + XMLNode root = new XMLNode(file); + + // The first source file is the root module. + String alloySourceFilename = root.getChildren(AlloyConstants.TRACE_SOURCE_TAG) + .iterator() + .next() + .getAttribute(AlloyConstants.TRACE_FILENAME_ATTR); + + for (XMLNode node : root) { + if (node.is(AlloyConstants.TRACE_SOURCE_TAG)) { + String sourceFilename = node.getAttribute(AlloyConstants.TRACE_FILENAME_ATTR); + Path sourceFilenamePath = Paths.get(sourceFilename); + Path mainFilePath = Paths.get(alloySourceFilename).getParent(); + sourceFilenamePath = mainFilePath.relativize(sourceFilenamePath); + + // Don't include Alloy standard library files. + if (sourceFilenamePath.startsWith("../")) { + continue; + } + + File outFile = tempDir.resolve(sourceFilenamePath).toFile(); + if (outFile.getParentFile() != null) { + outFile.getParentFile().mkdirs(); + } + + String sourceFileContents = node.getAttribute(AlloyConstants.TRACE_CONTENT_ATTR); + AlloyUtils.writeToFile(sourceFileContents, outFile); + } + } + + alloySourceFilename = tempDir.resolve(Paths.get(alloySourceFilename).getFileName()).toString(); + + // Parse from a file rather than a string in order to support includes. + CompModule module = CompUtil.parseEverything_fromFile(reporter, null, alloySourceFilename); + + return A4SolutionReader.read(module.getAllReachableSigs(), root); + } + + public static Sig getSigFromA4Solution(A4Solution sol, String sigName) { + for (Sig sig : sol.getAllReachableSigs()) { + if (sig.toString().equals(AlloyUtils.getLocallyNamespacedSigName(sigName))) { + return sig; + } + } + + return null; + } +} diff --git a/src/alloy/AlloyUtils.java b/src/alloy/AlloyUtils.java new file mode 100644 index 0000000..91ca926 --- /dev/null +++ b/src/alloy/AlloyUtils.java @@ -0,0 +1,196 @@ +package alloy; + +import java.io.BufferedWriter; +import java.io.IOException; +import java.io.FileWriter; +import java.io.File; +import java.nio.file.Files; +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.Set; + +public class AlloyUtils { + public static String getEmptyRelation(int arity) { + StringBuilder sb = new StringBuilder(); + sb.append(AlloyConstants.NONE); + for (int i = 1; i < arity; i++) { + sb.append(String.format(" -> %s", AlloyConstants.NONE)); + } + return sb.toString(); + } + + public static String getLocallyNamespacedSigName(String sigName) { + return AlloyConstants.THIS + sigName; + } + + /** + * getConcreteSigsDefinition returns Alloy code to define new signatures simulating scope. + * + * Complex models may include scopes for Sigs (e.g. in musical chairs, a scope may be 4 Player and + * 3 Chair). We need to keep track of these scopes throughout the transition system's execution, but + * Alloy syntax does not allow us to specify states of specific sig instances (for example, we are unable + * to write Alloy code to say that the fourth player is sitting on the second chair) - this means that we + * lose information about the execution state after every step, since we cannot encode the new state in the + * init predicate. + * + * To get around the aforementioned issue, we can inject new Sig definitions that are subsigs of the + * main Sig - we define concrete Sigs that we can easily refer to when defining the state. For example, + * if the scope of Player in musical chairs is 2, then we should define Player_1 and Player_2 sigs so + * we can refer to them when updating the init predicate. + * + * @param List + * @return String + */ + public static String getConcreteSigsDefinition(Map sigScopes) { + String concreteSigNameFormat = "%s_%d"; + String concreteSigsDefinitionFormat = "one sig %s extends %s {}\n"; + + StringBuilder concreteSigsSb = new StringBuilder(); + for (Map.Entry entry : sigScopes.entrySet()) { + if (entry.getValue() == 0) { + continue; + } + String sigName = entry.getKey(); + StringBuilder sigNamesSb = new StringBuilder(); + sigNamesSb.append(String.format(concreteSigNameFormat, sigName, 0)); + for (int i = 1; i < entry.getValue(); i++) { + sigNamesSb.append(", "); + sigNamesSb.append(String.format(concreteSigNameFormat, sigName, i)); + } + concreteSigsSb.append(String.format(concreteSigsDefinitionFormat, sigNamesSb.toString(), sigName)); + } + return concreteSigsSb.toString(); + } + + public static String makeStatePredicate(String predicateName, String stateSigName, String contents) { + String predicate = "\n" + + "pred %s[s: %s] {" + + "\n" + + "%s" + + "}" + + "\n"; + return String.format(predicate, predicateName, stateSigName, contents); + } + + /** + * annotatedTransitionSystem generates Alloy code based on the following rules: + * 1. Use ordering module. + * 2. Add fact to initialize state. + * 3. Add fact to define state transitions. + * 4. Add command to run state transitions. + */ + public static String annotatedTransitionSystem(String model, ParsingConf parsingConf, int steps, boolean until) { + String stateSigName = parsingConf.getStateSigName(); + String initPredicateName = parsingConf.getInitPredicateName(); + String transitionRelationName = parsingConf.getTransitionRelationName(); + Map additionalSigScopes = parsingConf.getAdditionalSigScopes(); + String transitionRelationFact = String.format( + "fact { all s: %s, s': s.next { %s[s, s'] } }" + "\n\n", stateSigName, transitionRelationName + ); + String sigScopes = String.format("run {%s} for exactly %d %s", until ? "break[last]" : "", steps + 1, stateSigName); + for (String sigScopeName : additionalSigScopes.keySet()) { + sigScopes += String.format(", exactly %d %s", additionalSigScopes.get(sigScopeName), sigScopeName); + } + return String.format( + String.format("open util/ordering[%s]" + "\n\n", stateSigName) + + model + "\n\n" + + String.format("fact { %s[first] }" + "\n\n", initPredicateName) + + transitionRelationFact + + sigScopes, + model + ); + } + + /** + * getBreakPredicate creates a predicate containing all breakpoints entered + * by the user. + * @param List, SigData + * @return String + */ + 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(), + predicateBody + ); + } + + /** + * createTmpFile creates a new file in the same directory as the given file. + * It then writes the contents into the new file and will delete it once the + * JVM terminates. This is required in Alloy to support models with user + * created imports as it can only find the submodules in the original file path. + * @param String, File + * @return File + */ + public static File createTmpFile(String contents, File file) throws IOException { + String filename = "_tmp_" + file.getName(); + File tmpFile = new File(file.getParentFile(), filename); + + writeToFile(contents, tmpFile); + tmpFile.deleteOnExit(); + + return tmpFile; + } + + public static void writeToFile(String contents, File file) throws IOException { + BufferedWriter writer = new BufferedWriter(new FileWriter(file)); + writer.write(contents); + writer.close(); + } + + public static String readFromFile(File file) throws IOException { + return new String(Files.readAllBytes(file.toPath())); + } + + /** + * getConstraint converts a raw (user-entered) constraint into a format + * accepted by Alloy. "s." is prepended to all references to a field in the + * raw constraint. This transformation enables constraints to be wrapped in + * a predicate that takes a State s as a parameter. + * @param String, Set + * @return String + */ + private static String getConstraint(String rawConstraint, Set fields) { + 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)) { + String field = buffer.toString(); + if (fields.contains(field)) { + String stateField = String.format("s.%s", field); + constraint.setLength(constraint.length() - field.length()); + constraint.append(stateField); + } + + buffer.setLength(0); + } else { + buffer.append(c); + } + + constraint.append(c); + } + + if (buffer.length() > 0) { + String field = buffer.toString(); + if (fields.contains(field)) { + String stateField = String.format("s.%s", field); + constraint.setLength(constraint.length() - field.length()); + constraint.append(stateField); + } + } + + return constraint.toString(); + } +} diff --git a/src/alloy/ParsingConf.java b/src/alloy/ParsingConf.java new file mode 100644 index 0000000..987a51e --- /dev/null +++ b/src/alloy/ParsingConf.java @@ -0,0 +1,85 @@ +package alloy; + +import org.yaml.snakeyaml.Yaml; +import org.yaml.snakeyaml.constructor.Constructor; +import org.yaml.snakeyaml.representer.Representer; + +import java.util.HashMap; +import java.util.Map; + +public class ParsingConf { + private static final String STATE_SIG_NAME_DEFAULT = "State"; + private static final String INIT_PREDICATE_NAME_DEFAULT = "init"; + private static final String TRANSITION_RELATION_NAME_DEFAULT = "next"; + + // Important keywords that are parsed/observed in the comments of an Alloy model file for configuration. + public final static String BEGIN_ALDB_CONF = "BEGIN_ALDB_CONF"; + public final static String END_ALDB_CONF = "END_ALDB_CONF"; + private final static String ESCAPED_CHARACTERS = "[/*]"; + + // Name of the sig representing the main state in the Alloy model. + private String stateSigName; + // Name of the predicate which defines the initial state in the Alloy model. + private String initPredicateName; + // Name of the transition relation in the Alloy model. + private String transitionRelationName; + // Additional Alloy sig scopes to specify. + private Map additionalSigScopes; + + public ParsingConf() { + stateSigName = STATE_SIG_NAME_DEFAULT; + initPredicateName = INIT_PREDICATE_NAME_DEFAULT; + transitionRelationName = TRANSITION_RELATION_NAME_DEFAULT; + additionalSigScopes = new HashMap<>(); + } + + public static ParsingConf initializeWithYaml(String file) { + Representer representer = new Representer(); + representer.getPropertyUtils().setSkipMissingProperties(true); + Yaml yaml = new Yaml(new Constructor(ParsingConf.class), representer); + return yaml.loadAs(file, ParsingConf.class); + } + + public void setStateSigName(String stateSigName) { + this.stateSigName = stateSigName; + } + + public String getStateSigName() { + return stateSigName; + } + + public void setInitPredicateName(String initPredicateName) { + this.initPredicateName = initPredicateName; + } + + public String getInitPredicateName() { + return initPredicateName; + } + + public void setTransitionRelationName(String transitionRelationName) { + this.transitionRelationName = transitionRelationName; + } + + public String getTransitionRelationName() { + return transitionRelationName; + } + + public void setAdditionalSigScopes(Map additionalSigScopes) { + this.additionalSigScopes = additionalSigScopes; + } + + public Map getAdditionalSigScopes() { + return additionalSigScopes; + } + + public static String getConfStringFromFileString(String file) { + String config = ""; + int fileStartIdx = file.indexOf(BEGIN_ALDB_CONF); + int fileEndIdx = file.indexOf(END_ALDB_CONF); + + if (fileStartIdx == -1 || fileEndIdx == -1) return config; + + config = file.substring(fileStartIdx + BEGIN_ALDB_CONF.length(), fileEndIdx-1).replaceAll(ESCAPED_CHARACTERS, ""); + return config; + } +} diff --git a/src/alloy/SigData.java b/src/alloy/SigData.java new file mode 100644 index 0000000..2c90764 --- /dev/null +++ b/src/alloy/SigData.java @@ -0,0 +1,51 @@ +package alloy; + +import edu.mit.csail.sdg.ast.Sig; +import edu.mit.csail.sdg.ast.Type; + +import java.util.HashMap; +import java.util.Map; +import java.util.Set; + +public class SigData { + private String label; + // Map of field name to Type. + private Map data; + + public SigData(Sig sig) { + label = sig.label; + data = new HashMap<>(); + for (Sig.Field field : sig.getFields()) { + data.put(field.label, field.type()); + } + } + + public String getLabel() { + return label; + } + + public Set getFields() { + return data.keySet(); + } + + public String getTypeForField(String field) { + Type type = data.get(field); + + if (type == null) { + return null; + } + + return type.toString(); + } + + public int getArityForField(String field) { + Type type = data.get(field); + + if (type == null) { + return 0; + } + + // Subtract one from arity to ignore the default relation from the State sig. + return type.arity() - 1; + } +} diff --git a/src/commands/AltCommand.java b/src/commands/AltCommand.java new file mode 100644 index 0000000..3e3847d --- /dev/null +++ b/src/commands/AltCommand.java @@ -0,0 +1,47 @@ +package commands; + +import simulation.SimulationManager; + +public class AltCommand extends Command { + private final static String R_FLAG = "-r"; + + public String getName() { + return CommandConstants.ALT_NAME; + } + + public String[] getShorthand() { + return CommandConstants.ALT_SHORTHAND; + } + + public String getDescription() { + return CommandConstants.ALT_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.ALT_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + boolean reverse = false; + if (input.length != 1) { + if (input[1].equals(R_FLAG)) { + reverse = true; + } else { + System.out.println(CommandConstants.ALT_HELP); + return; + } + } + + if (!simulationManager.selectAlternatePath(reverse)) { + System.out.println(CommandConstants.ALT_UNAVAILABLE); + return; + } + + System.out.println(simulationManager.getCurrentStateString()); + } +} diff --git a/src/commands/BreakCommand.java b/src/commands/BreakCommand.java new file mode 100644 index 0000000..c0493c5 --- /dev/null +++ b/src/commands/BreakCommand.java @@ -0,0 +1,80 @@ +package commands; + +import simulation.ConstraintManager; +import simulation.SimulationManager; + +import java.util.Arrays; +import java.util.Map; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class BreakCommand extends Command { + private final static String RM_FLAG = "-rm"; + private final static String L_FLAG = "-l"; + private final static String C_FLAG = "-c"; + + public String getName() { + return CommandConstants.BREAK_NAME; + } + + public String getDescription() { + return CommandConstants.BREAK_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.BREAK_HELP; + } + + public String[] getShorthand() { + return CommandConstants.BREAK_SHORTHAND; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (input.length == 1) { + System.out.println(CommandConstants.BREAK_HELP); + return; + } + String arg = input[1]; + + ConstraintManager cm = simulationManager.getConstraintManager(); + if (arg.equals(RM_FLAG)) { + if (input.length != 3) { + System.out.println(CommandConstants.BREAK_HELP); + return; + } + int constraintID; + try { + constraintID = Integer.parseInt(input[2]); + } catch (NumberFormatException e) { + System.out.println(CommandConstants.INTEGER_ERROR); + return; + } + if (!cm.removeConstraint(constraintID)) { + System.out.println(String.format(CommandConstants.INVALID_CONSTRAINT_ID, constraintID)); + } + } else if (arg.equals(L_FLAG)) { + System.out.println(cm.getFormattedConstraints()); + } else if (arg.equals(C_FLAG)) { + cm.clearConstraints(); + } else { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + // Use regex to find constraints delimited by spaces, and encapsulated by quotes. + // Example: 'break "a = b" c' should add two constraints, "a = b" and "c". + String allConstraints = String.join(" ", Arrays.copyOfRange(input, 1, input.length)); + Matcher m = Pattern.compile(CommandConstants.CONSTRAINT_REGEX).matcher(allConstraints); + + while (m.find()) { + String constraint = m.group(1).replace("\"", ""); + + if (simulationManager.validateConstraint(constraint)) { + cm.addConstraint(constraint); + } else { + System.out.println(String.format(CommandConstants.INVALID_CONSTRAINT, constraint)); + } + } + } + } +} diff --git a/src/commands/Command.java b/src/commands/Command.java new file mode 100644 index 0000000..09f8723 --- /dev/null +++ b/src/commands/Command.java @@ -0,0 +1,21 @@ +package commands; + +import simulation.SimulationManager; + +public abstract class Command { + private final static String[] SHORTHAND = {}; + + public abstract String getName(); + public abstract String getDescription(); + public abstract String getHelp(); + + public abstract void execute(String[] input, SimulationManager simulationManager); + + public String[] getShorthand() { + return SHORTHAND; + } + + public boolean requiresFile() { + return false; + } +} diff --git a/src/commands/CommandConstants.java b/src/commands/CommandConstants.java new file mode 100644 index 0000000..dcf6d7d --- /dev/null +++ b/src/commands/CommandConstants.java @@ -0,0 +1,136 @@ +package commands; + +public class CommandConstants { + public final static String DONE = "done."; + public final static String READING_MODEL = "Reading model from %s..."; + 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"; + public final static String NO_FILE_SPECIFIED = "Error. No file specified."; + public final static String IO_FAILED = "error. I/O failed."; + public final static String FAILED_TO_READ_FILE = "error. Failed to read file."; + public final static String FAILED_TO_READ_CONF = "error. Invalid configuration."; + public final static String INVALID_TRACE = "error. Invalid trace."; + public final static String TMP_FILE_ERROR = "internal error. Failed to create temporary Alloy file."; + public final static String SETTING_PARSING_OPTIONS = "Setting default parsing options..."; + public final static String SETTING_PARSING_OPTIONS_FROM = "Setting parsing options from %s..."; + public final static String UNDEFINED_COMMAND = "Undefined command: \"%s\". Try \"help\".\n"; + public final static String AVAILABLE_COMMANDS_STR = "Available commands:\n\n"; + public final static String COMMAND_HELP_DELIMITER = "%-15s-- %s\n"; + public final static String INTEGER_ERROR = "Error. Input must be an integer."; + public final static String GR_ONE_ERROR = "Error. Input must be >= 1."; + public final static String SIG_NOT_FOUND = "Signature not found."; + public final static String ALT_UNAVAILABLE = "No alternate execution paths."; + public final static String UNTIL_FAILED = "Unable to find satisfying solution."; + public final static String NO_MODEL_LOADED = "No model file specified.\nUse the \"load\" command."; + + public final static String CURRENT_NAME = "current"; + public final static String CURRENT_DESCRIPTION = "Display the current state"; + public final static String CURRENT_HELP = "Display the current state.\n\n" + + "Usage: current [property]\n\n" + + "By default, all properties are printed."; + public final static String[] CURRENT_SHORTHAND = {"c", "curr"}; + + public final static String HELP_NAME = "help"; + public final static String HELP_DESCRIPTION = "Display the list of available commands"; + public final static String[] HELP_SHORTHAND = {"h"}; + public final static String HELP_COMMAND_END_STR = "\nType \"help\" followed by a command name for full documentation."; + + public final static String LOAD_NAME = "load"; + public final static String LOAD_DESCRIPTION = "Load an Alloy model"; + public final static String LOAD_HELP = "Load an Alloy model.\n\n" + + "Usage: load \n\n" + + "The specified file must be an Alloy (.als) file.\n\n" + + "You can also specify custom parsing options for this Alloy model as a comment.\n" + + "The comment block needs to have a header as: BEGIN_ALDB_CONF and a footer as: END_ALDB_CONF.\n" + + "The configuration format follows the YAML format for the setconf command."; + public final static String[] LOAD_SHORTHAND = {"l", "ld"}; + + public final static String QUIT_NAME = "quit"; + public final static String QUIT_DESCRIPTION = "Exit ALDB"; + public final static String QUIT_HELP = "Exit ALDB\n\n" + + "Confirmation is required when attempting to quit during an active debugging session."; + public final static String[] QUIT_SHORTHAND = {"q", "exit"}; + public final static String QUIT_USER_PROMPT = "A debugging session is active.\nQuit anyway? (y or n) "; + public final static String[] QUIT_ACCEPTED_RESPONSES = {"y", "Y", "yes", "Yes"}; + + public final static String[] REVERSE_STEP_SHORTHAND = {"rs", "r"}; + public final static String REVERSE_STEP_NAME = "reverse-step"; + public final static String REVERSE_STEP_DESCRIPTION = "Go back n steps in the current state traversal path"; + public final static String REVERSE_STEP_HELP = "Go back n steps in the current state traversal path.\n\n" + + "Usage: reverse-step [n]\n\n" + + "n is an integer >= 1. By default, n = 1."; + + public final static String SETCONF_NAME = "setconf"; + public final static String SETCONF_DESCRIPTION = "Set parsing options for the current session"; + public final static String SETCONF_HELP = "Set custom parsing options for the current session.\n\n" + + "Usage: setconf [filename]\n\n" + + "The specified file must be in YAML. The following (customizable) properties are set by default:\n\n" + + "# Name of the sig representing the main state in the Alloy model.\n" + + "stateSigName: State\n" + + "# Name of the predicate which defines the initial state in the Alloy model.\n" + + "initPredicateName: init\n" + + "# Name of the transition relation in the Alloy model.\n" + + "transitionRelationName: next\n" + + "# Additional Alloy sig scopes to specify.\n" + + "additionalSigScopes: {}\n\n" + + "Running setconf with no filename will set the above default options."; + + public final static String STEP_NAME = "step"; + public final static String STEP_DESCRIPTION = "Perform a state transition of n steps"; + public final static String STEP_HELP = "Perform a state transition of n steps.\n\n" + + "Usage: step [n]\n\n" + + "n must be an integer >= 1. By default, n = 1."; + public final static String[] STEP_SHORTHAND = {"s", "st"}; + + public final static String TRACE_NAME = "trace"; + public final static String TRACE_DESCRIPTION = "Load a saved Alloy XML instance"; + public final static String TRACE_HELP = "Load a saved Alloy XML instance.\n\n" + + "Usage: trace \n\n" + + "The specified file should be in the Alloy XML format."; + public final static String[] TRACE_SHORTHAND = {"t"}; + + public final static String HISTORY_NAME = "history"; + public final static String HISTORY_DESCRIPTION = "Display past states"; + public final static String HISTORY_HELP = "Display the past n consecutive states of the active execution path.\n\n" + + "Usage: history [n]\n\n" + + "n must be an integer >= 1. By default, n = 3."; + + public final static String SCOPE_NAME = "scope"; + public final static String SCOPE_DESCRIPTION = "Display scope set"; + public final static String SCOPE_HELP = "Display the scope set of the active model.\n\n" + + "Usage: scope [sig-name]\n\n" + + "By default, scope sets are displayed for all signatures in the model."; + + public final static String ALT_NAME = "alt"; + public final static String ALT_DESCRIPTION = "Select an alternate execution path"; + public final static String ALT_HELP = "Select an alternate execution path.\n\n" + + "Usage: alt [-r]\n\n" + + "If \"-r\" is specified, the previous execution path is selected."; + public final static String[] ALT_SHORTHAND = {"a"}; + + public final static String BREAK_NAME = "break"; + public final static String BREAK_DESCRIPTION = "Control the set of constraints used"; + public final static String BREAK_HELP = "Control the set of constraints used.\n\n" + + "Usage:\n\n" + + "break -- Add a constraint\n" + + "break -rm -- Remove a constraint\n" + + "break -l -- List all constraints\n" + + "break -c -- Clear constraints"; + public final static String CONSTRAINT_REGEX = "([^\"]\\S*|\".+?\")\\s*"; + public final static String INVALID_CONSTRAINT_ID = "No constraint number %d."; + public final static String INVALID_CONSTRAINT = "Invalid constraint: \"%s\"."; + public final static String[] BREAK_SHORTHAND = {"b"}; + + public final static String UNTIL_NAME = "until"; + public final static String UNTIL_DESCRIPTION = "Run until constraints are met"; + public final static String UNTIL_HELP = "Run until constraints are met.\n\n" + + "Usage: until [limit]\n\n" + + "limit must be an integer >= 1. By default, limit = 10."; + public final static String[] UNTIL_SHORTHAND = {"u"}; + + public final static String DOT_NAME = "dot"; + 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"}; +} diff --git a/src/commands/CommandRegistry.java b/src/commands/CommandRegistry.java new file mode 100644 index 0000000..dc255c3 --- /dev/null +++ b/src/commands/CommandRegistry.java @@ -0,0 +1,46 @@ +package commands; + +public final class CommandRegistry { + public final static Command NOT_FOUND = new NotFoundCommand(); + public final static Command EMPTY = new EmptyCommand(); + private final static Command[] commands = { + new AltCommand(), + new BreakCommand(), + new CurrentCommand(), + new DotCommand(), + new HelpCommand(), + new HistoryCommand(), + new LoadCommand(), + new QuitCommand(), + new ReverseStepCommand(), + new SetConfCommand(), + new ScopeCommand(), + new StepCommand(), + new TraceCommand(), + new UntilCommand(), + }; + + public static Command commandForString(String string) { + if (string.isEmpty()) { + return EMPTY; + } + for (Command command : commands) { + if (command.getName().equals(string)) { + return command; + } + + String[] shorthand = command.getShorthand(); + for (String s : shorthand) { + if (s.equals(string)) { + return command; + } + } + } + + return NOT_FOUND; + } + + public static Command[] getAllCommands() { + return commands; + } +} diff --git a/src/commands/CurrentCommand.java b/src/commands/CurrentCommand.java new file mode 100644 index 0000000..a79fa53 --- /dev/null +++ b/src/commands/CurrentCommand.java @@ -0,0 +1,37 @@ +package commands; + +import simulation.SimulationManager; + +public class CurrentCommand extends Command { + private final static String[] SHORTHAND = CommandConstants.CURRENT_SHORTHAND; + + public String getName() { + return CommandConstants.CURRENT_NAME; + } + + public String getDescription() { + return CommandConstants.CURRENT_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.CURRENT_HELP; + } + + public String[] getShorthand() { + return SHORTHAND; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + if (input.length == 1) { + System.out.println(simulationManager.getCurrentStateString()); + return; + } + String property = input[1]; + System.out.println(simulationManager.getCurrentStateStringForProperty(property)); + } +} diff --git a/src/commands/DotCommand.java b/src/commands/DotCommand.java new file mode 100644 index 0000000..df39ab0 --- /dev/null +++ b/src/commands/DotCommand.java @@ -0,0 +1,50 @@ +package commands; + +import alloy.AlloyUtils; +import simulation.SimulationManager; + +import java.io.File; +import java.io.IOException; +import java.text.SimpleDateFormat; +import java.util.Date; + +public class DotCommand extends Command { + private final String FILE_PREFIX = "aldb."; + private final String DATE_FORMAT = "yyyy.MM.dd.HH.mm.ss"; + private final String EXT = ".gv"; + + public String getName() { + return CommandConstants.DOT_NAME; + } + + public String getDescription() { + return CommandConstants.DOT_DESCRIPTION; + } + + public String[] getShorthand() { + return CommandConstants.DOT_SHORTHAND; + } + + public String getHelp() { + return CommandConstants.DOT_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + String filename = FILE_PREFIX + new SimpleDateFormat(DATE_FORMAT).format(new Date()) + EXT; + System.out.printf(CommandConstants.WRITING_DOT_GRAPH, filename); + + File f = new File(simulationManager.getWorkingDirPath(), filename); + try { + f.createNewFile(); + AlloyUtils.writeToFile(simulationManager.getDOTString(), f); + System.out.println(CommandConstants.DONE); + } catch (IOException e) { + System.out.println(CommandConstants.IO_FAILED); + } + } +} diff --git a/src/commands/EmptyCommand.java b/src/commands/EmptyCommand.java new file mode 100644 index 0000000..11edb32 --- /dev/null +++ b/src/commands/EmptyCommand.java @@ -0,0 +1,20 @@ +package commands; + +import simulation.SimulationManager; + +public class EmptyCommand extends Command { + public String getName() { + return null; + } + + public String getDescription() { + return null; + } + + public String getHelp() { + return null; + } + + public void execute(String[] input, SimulationManager simulationManager) {} +} + diff --git a/src/commands/HelpCommand.java b/src/commands/HelpCommand.java new file mode 100644 index 0000000..098f220 --- /dev/null +++ b/src/commands/HelpCommand.java @@ -0,0 +1,42 @@ +package commands; + +import simulation.SimulationManager; + +import java.lang.StringBuilder; + +public class HelpCommand extends Command { + public String getName() { + return CommandConstants.HELP_NAME; + } + + public String getDescription() { + return CommandConstants.HELP_DESCRIPTION; + } + + public String[] getShorthand() { + return CommandConstants.HELP_SHORTHAND; + } + + public String getHelp() { + StringBuilder sb = new StringBuilder(); + sb.append(CommandConstants.AVAILABLE_COMMANDS_STR); + for (Command command : CommandRegistry.getAllCommands()) { + sb.append(String.format(CommandConstants.COMMAND_HELP_DELIMITER, command.getName(), command.getDescription())); + } + sb.append(CommandConstants.HELP_COMMAND_END_STR); + return sb.toString(); + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (input.length < 2) { + System.out.println(getHelp()); + } else { + Command command = CommandRegistry.commandForString(input[1]); + if (command == CommandRegistry.NOT_FOUND) { + System.out.println(getHelp()); + } else { + System.out.println(command.getHelp()); + } + } + } +} diff --git a/src/commands/HistoryCommand.java b/src/commands/HistoryCommand.java new file mode 100644 index 0000000..680e436 --- /dev/null +++ b/src/commands/HistoryCommand.java @@ -0,0 +1,41 @@ +package commands; + +import simulation.SimulationManager; + +public class HistoryCommand extends Command { + public String getName() { + return CommandConstants.HISTORY_NAME; + } + + public String getDescription() { + return CommandConstants.HISTORY_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.HISTORY_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + int n = 3; + if (input.length > 1) { + try { + n = Integer.parseInt(input[1]); + } catch (NumberFormatException e) { + System.out.println(CommandConstants.INTEGER_ERROR); + return; + } + } + + if (n < 1) { + System.out.println(CommandConstants.GR_ONE_ERROR); + return; + } + + System.out.println(simulationManager.getHistory(n)); + } +} diff --git a/src/commands/LoadCommand.java b/src/commands/LoadCommand.java new file mode 100644 index 0000000..23c3f37 --- /dev/null +++ b/src/commands/LoadCommand.java @@ -0,0 +1,66 @@ +package commands; + +import alloy.AlloyUtils; +import simulation.SimulationManager; + +import java.io.IOException; +import java.io.File; +import java.nio.file.Files; + +public class LoadCommand extends Command { + public String getName() { + return CommandConstants.LOAD_NAME; + } + + public String getDescription() { + return CommandConstants.LOAD_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.LOAD_HELP; + } + + public String[] getShorthand() { + return CommandConstants.LOAD_SHORTHAND; + } + + public boolean requiresFile() { + return true; + } + + public void execute(String[] input, SimulationManager 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); + + String inputFileContents; + try { + inputFileContents = AlloyUtils.readFromFile(file); + } catch (IOException e) { + System.out.println(CommandConstants.FAILED_TO_READ_FILE); + return; + } + + File tmpModelFile; + try { + tmpModelFile = AlloyUtils.createTmpFile(inputFileContents, file); + } catch (IOException e) { + System.out.println(CommandConstants.TMP_FILE_ERROR); + return; + } + + if (simulationManager.initializeWithModel(tmpModelFile)) { + System.out.println(CommandConstants.DONE); + } + } +} diff --git a/src/commands/NotFoundCommand.java b/src/commands/NotFoundCommand.java new file mode 100644 index 0000000..01a9eb8 --- /dev/null +++ b/src/commands/NotFoundCommand.java @@ -0,0 +1,21 @@ +package commands; + +import simulation.SimulationManager; + +public class NotFoundCommand extends Command { + public String getName() { + return null; + } + + public String getDescription() { + return null; + } + + public String getHelp() { + return null; + } + + public void execute(String[] input, SimulationManager simulationManager) { + System.out.printf(CommandConstants.UNDEFINED_COMMAND, input[0]); + } +} diff --git a/src/commands/QuitCommand.java b/src/commands/QuitCommand.java new file mode 100644 index 0000000..5c7d511 --- /dev/null +++ b/src/commands/QuitCommand.java @@ -0,0 +1,35 @@ +package commands; + +import simulation.SimulationManager; + +public class QuitCommand extends Command { + public String getName() { + return CommandConstants.QUIT_NAME; + } + + public String getDescription() { + return CommandConstants.QUIT_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.QUIT_HELP; + } + + public String[] getShorthand() { + return CommandConstants.QUIT_SHORTHAND; + } + + public void execute(String[] input, SimulationManager simulationManager) { + // Only require user confirmation when they are in an active simulation. + if (!simulationManager.isInitialized()) { + System.exit(0); + } + System.out.print(CommandConstants.QUIT_USER_PROMPT); + String s = System.console().readLine(); + for (String accepted : CommandConstants.QUIT_ACCEPTED_RESPONSES) { + if (s.equals(accepted)) { + System.exit(0); + } + } + } +} diff --git a/src/commands/ReverseStepCommand.java b/src/commands/ReverseStepCommand.java new file mode 100644 index 0000000..3423233 --- /dev/null +++ b/src/commands/ReverseStepCommand.java @@ -0,0 +1,45 @@ +package commands; + +import simulation.SimulationManager; + +public class ReverseStepCommand extends Command { + public String getName() { + return CommandConstants.REVERSE_STEP_NAME; + } + + public String[] getShorthand() { + return CommandConstants.REVERSE_STEP_SHORTHAND; + } + + public String getDescription() { + return CommandConstants.REVERSE_STEP_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.REVERSE_STEP_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + int steps = 1; + if (input.length > 1) { + try { + steps = Integer.parseInt(input[1]); + } catch (NumberFormatException e) { + System.out.println(CommandConstants.INTEGER_ERROR); + return; + } + } + + if (steps < 1) { + System.out.println(CommandConstants.GR_ONE_ERROR); + return; + } + + simulationManager.performReverseStep(steps); + } +} diff --git a/src/commands/ScopeCommand.java b/src/commands/ScopeCommand.java new file mode 100644 index 0000000..47ed5eb --- /dev/null +++ b/src/commands/ScopeCommand.java @@ -0,0 +1,52 @@ +package commands; + +import alloy.AlloyConstants; +import simulation.SimulationManager; + +import java.util.List; +import java.util.Map; + +public class ScopeCommand extends Command { + public String getName() { + return CommandConstants.SCOPE_NAME; + } + + public String getDescription() { + return CommandConstants.SCOPE_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.SCOPE_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + if (input.length == 1) { + System.out.println(); + Map> scopes = simulationManager.getScopes(); + for (String label : scopes.keySet()) { + StringBuilder sb = new StringBuilder(); + sb.append(String.format("%s: %s ", label, AlloyConstants.BLOCK_INITIALIZER)); + sb.append(String.format("%s %s", String.join(", ", scopes.get(label)), AlloyConstants.BLOCK_TERMINATOR)); + System.out.println(sb.toString()); + } + System.out.println(); + return; + } + String sigName = input[1]; + List scope = simulationManager.getScopeForSig(sigName); + if (scope == null) { + System.out.println(CommandConstants.SIG_NOT_FOUND); + return; + } + System.out.println(); + for (String s : scope) { + System.out.println(s); + } + System.out.println(); + } +} diff --git a/src/commands/SetConfCommand.java b/src/commands/SetConfCommand.java new file mode 100644 index 0000000..db8c9a4 --- /dev/null +++ b/src/commands/SetConfCommand.java @@ -0,0 +1,61 @@ +package commands; + +import alloy.AlloyUtils; +import alloy.ParsingConf; +import simulation.SimulationManager; + +import java.io.IOException; +import java.io.File; +import java.nio.file.Files; + +import org.yaml.snakeyaml.error.YAMLException; + +public class SetConfCommand extends Command { + public SetConfCommand() {} + + public String getName() { + return CommandConstants.SETCONF_NAME; + } + + public String getDescription() { + return CommandConstants.SETCONF_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.SETCONF_HELP; + } + + public boolean requiresFile() { + return true; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (input.length < 2) { + System.out.print(CommandConstants.SETTING_PARSING_OPTIONS); + simulationManager.setParsingConf(new ParsingConf()); + System.out.println(CommandConstants.DONE); + return; + } + + String filename = input[1]; + File file = new File(filename); + + System.out.printf(CommandConstants.SETTING_PARSING_OPTIONS_FROM, filename); + + String inputFileContents; + try { + inputFileContents = AlloyUtils.readFromFile(file); + } catch (IOException e) { + System.out.println(CommandConstants.FAILED_TO_READ_FILE); + return; + } + try { + ParsingConf conf = ParsingConf.initializeWithYaml(inputFileContents); + simulationManager.setParsingConf(conf); + } catch (YAMLException e) { + System.out.println(CommandConstants.FAILED_TO_READ_CONF); + return; + } + System.out.println(CommandConstants.DONE); + } +} diff --git a/src/commands/StepCommand.java b/src/commands/StepCommand.java new file mode 100644 index 0000000..fa7cd44 --- /dev/null +++ b/src/commands/StepCommand.java @@ -0,0 +1,54 @@ +package commands; + +import simulation.SimulationManager; + +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; + } + + public String getHelp() { + return CommandConstants.STEP_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + int steps = 1; + if (input.length > 1) { + try { + steps = Integer.parseInt(input[1]); + } catch (NumberFormatException e) { + System.out.println(CommandConstants.INTEGER_ERROR); + return; + } + } + + if (steps < 1) { + System.out.println(CommandConstants.GR_ONE_ERROR); + return; + } + + simulationManager.performStep(steps); + + if (simulationManager.isTrace()) { + System.out.println(simulationManager.getCurrentStateDiffString()); + return; + } + + System.out.println(simulationManager.getCurrentStateString()); + } +} diff --git a/src/commands/TraceCommand.java b/src/commands/TraceCommand.java new file mode 100644 index 0000000..dd0268c --- /dev/null +++ b/src/commands/TraceCommand.java @@ -0,0 +1,52 @@ +package commands; + +import simulation.SimulationManager; + +import java.io.File; + +public class TraceCommand extends Command { + private final static String[] SHORTHAND = CommandConstants.TRACE_SHORTHAND; + + public String getName() { + return CommandConstants.TRACE_NAME; + } + + public String getDescription() { + return CommandConstants.TRACE_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.TRACE_HELP; + } + + public String[] getShorthand() { + return SHORTHAND; + } + + public boolean requiresFile() { + return true; + } + + public void execute(String[] input, SimulationManager 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_TRACE, filename); + + if (!simulationManager.initializeWithTrace(file)) { + System.out.println(CommandConstants.INVALID_TRACE); + return; + } + + System.out.println(CommandConstants.DONE); + } +} diff --git a/src/commands/UntilCommand.java b/src/commands/UntilCommand.java new file mode 100644 index 0000000..eb02da5 --- /dev/null +++ b/src/commands/UntilCommand.java @@ -0,0 +1,50 @@ +package commands; + +import simulation.SimulationManager; + +public class UntilCommand extends Command { + public String getName() { + return CommandConstants.UNTIL_NAME; + } + + public String[] getShorthand() { + return CommandConstants.UNTIL_SHORTHAND; + } + + public String getDescription() { + return CommandConstants.UNTIL_DESCRIPTION; + } + + public String getHelp() { + return CommandConstants.UNTIL_HELP; + } + + public void execute(String[] input, SimulationManager simulationManager) { + if (!simulationManager.isInitialized()) { + System.out.println(CommandConstants.NO_MODEL_LOADED); + return; + } + + int limit = 10; + if (input.length > 1) { + try { + limit = Integer.parseInt(input[1]); + } catch (NumberFormatException e) { + System.out.println(CommandConstants.INTEGER_ERROR); + return; + } + } + + if (limit < 1) { + System.out.println(CommandConstants.GR_ONE_ERROR); + return; + } + + if (!simulationManager.performUntil(limit)) { + System.out.println(CommandConstants.UNTIL_FAILED); + return; + } + + System.out.println(simulationManager.getCurrentStateString()); + } +} diff --git a/src/core/CLI.java b/src/core/CLI.java new file mode 100644 index 0000000..8368dd8 --- /dev/null +++ b/src/core/CLI.java @@ -0,0 +1,91 @@ +package core; + +import commands.*; + +import java.io.IOException; +import java.util.ArrayList; +import java.util.List; +import java.util.HashMap; +import java.util.Map; + +import org.jline.builtins.Completers.FileNameCompleter; +import org.jline.builtins.Completers.RegexCompleter; +import org.jline.reader.Completer; +import org.jline.reader.EndOfFileException; +import org.jline.reader.LineReader; +import org.jline.reader.LineReaderBuilder; +import org.jline.reader.UserInterruptException; +import org.jline.reader.impl.completer.StringsCompleter; +import org.jline.reader.impl.DefaultParser; +import org.jline.terminal.*; + +class CLI { + private static final String PROMPT = "(aldb) "; + + private LineReader reader; + + public CLI() { + Terminal terminal = null; + try { + terminal = TerminalBuilder.builder().system(true).build(); + } catch (IOException e) { + System.exit(0); + } + + Completer completer = createCompleter(); + + DefaultParser parser = new DefaultParser(); + parser.setEofOnUnclosedQuote(true); + + reader = LineReaderBuilder + .builder() + .terminal(terminal) + .completer(completer) + .parser(parser) + .build(); + } + + public String[] getInput() { + String rawInput = null; + try { + rawInput = reader.readLine(PROMPT); + } catch (UserInterruptException e) { + System.exit(0); + } catch (EndOfFileException e) { + System.exit(0); + } + + String[] input = {}; + if (rawInput != null) { + input = rawInput.trim().split(" "); + } + + return input; + } + + private Completer createCompleter() { + Map completers = new HashMap<>(); + List regex = new ArrayList(); + + int commandID = 1; + completers.put("file", new FileNameCompleter()); + for (Command command : CommandRegistry.getAllCommands()) { + // The completer name is different from the command name to allow + // for commands containing special characters (such as hyphens) + // to be understood by the RegexCompleter. + String commandName = command.getName(); + String completerName = String.format("C%d", commandID); + completers.put(completerName, new StringsCompleter(commandName)); + + if (command.requiresFile()) { + regex.add(String.format("%s file", completerName)); + } else { + regex.add(completerName); + } + + commandID++; + } + + return new RegexCompleter(String.join("|", regex), completers::get); + } +} diff --git a/src/core/Main.java b/src/core/Main.java new file mode 100644 index 0000000..6b57a6f --- /dev/null +++ b/src/core/Main.java @@ -0,0 +1,98 @@ +package core; + +import commands.Command; +import commands.CommandConstants; +import commands.CommandRegistry; +import simulation.SimulationManager; +import net.sourceforge.argparse4j.ArgumentParsers; +import net.sourceforge.argparse4j.impl.Arguments; +import net.sourceforge.argparse4j.inf.ArgumentParser; +import net.sourceforge.argparse4j.inf.ArgumentParserException; +import net.sourceforge.argparse4j.inf.Namespace; + +import java.io.IOException; + +public class Main { + private static SimulationManager simulationManager; + private static SessionLog log; + private static String prevSessionLogPath; + + private static String PROGRAM_NAME = "Alloy Debugger (ALDB)"; + private static String VERSION = "0.1.0"; + private static String PROGRAM_DESC = "A debugger for transition systems modelled in Alloy."; + + private static String RESTORE_FLAG_SHORT = "-r"; + private static String RESTORE_FLAG = "--restore"; + private static String RESTORE_DESC = "restore session from existing session log file"; + private static String VERSION_FLAG_SHORT = "-v"; + private static String VERSION_FLAG = "--version"; + private static String VERSION_DESC = "show version information and exit"; + + private static String FILE_ARG_NAME = "file"; + private static String FILE_ARG_DESC = "Alloy model to load on start-up"; + private static String OPTIONAL = "?"; + + private static String CREATE_LOG_ERROR = "Error. Unable to create session log. Continuing without session log."; + private static String RESTORING_SESSION_TEXT = "Restoring session from session log \"%s\"."; + private static String SESSION_LOG_OPEN_ERROR = "Error. Session log \"%s\" could not be opened for reading. Continuing with new empty session log."; + + public static void main(String[] args) throws IOException { + ArgumentParser parser = ArgumentParsers.newFor(PROGRAM_NAME).build() + .defaultHelp(true) + .description(PROGRAM_DESC) + .version(String.format("${prog} v%s", VERSION)); + 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); + + Namespace ns = null; + try { + ns = parser.parseArgs(args); + } catch (ArgumentParserException e) { + parser.handleError(e); + System.exit(1); + } + + simulationManager = new SimulationManager(); + CLI cli = new CLI(); + + // Pre-load a model if its path is passed in on start-up. + String modelPath = ns.getString(FILE_ARG_NAME); + if (modelPath != null) { + String[] input = { CommandConstants.LOAD_NAME, modelPath }; + Command command = CommandRegistry.commandForString(input[0]); + command.execute(input, simulationManager); + } + + log = new SessionLog(null); + try { + log.create(); + } catch (IOException e) { + System.out.println(CREATE_LOG_ERROR); + } + + // Attempt to restore a previous session if the restore flag is used. + prevSessionLogPath = ns.getString(RESTORE_FLAG.substring(2)); // Drop leading `--`. + if (prevSessionLogPath != null) { + System.out.println(String.format(RESTORING_SESSION_TEXT, prevSessionLogPath)); + SessionLog prevLog = null; + try { + prevLog = new SessionLog(prevSessionLogPath); + } catch (IOException e) { + System.out.println(String.format(SESSION_LOG_OPEN_ERROR, prevSessionLogPath)); + } + if (prevLog != null) { + prevLog.restore(simulationManager, log); + } + } + + while (true) { + String[] input = cli.getInput(); + Command command = CommandRegistry.commandForString(input[0]); + command.execute(input, simulationManager); + if (log.isInitialized()) { + log.append(input); + } + } + } +} diff --git a/src/core/SessionLog.java b/src/core/SessionLog.java new file mode 100644 index 0000000..41e4ca1 --- /dev/null +++ b/src/core/SessionLog.java @@ -0,0 +1,75 @@ +package core; + +import commands.Command; +import commands.CommandRegistry; +import simulation.SimulationManager; + +import java.io.BufferedReader; +import java.io.File; +import java.io.FileReader; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; +import java.nio.file.StandardOpenOption; +import java.text.SimpleDateFormat; +import java.util.Date; + +/** + * SessionLog is an append-only log on disk of commands that the user has submitted. + * + * For example, the contents of the log can look like: + * + * help + * load model.als + * step + * step 4 + * foo + */ +public class SessionLog { + private File log; + private BufferedReader br; + private String FILE_PREFIX = "aldb."; + private String DATE_FORMAT = "yyyy.MM.dd.HH.mm.ss"; + private String TMP_DIR_PROPERTY = "java.io.tmpdir"; + private String WHITESPACE_REGEX = "\\s+"; + + public SessionLog(String prevLogPath) throws IOException { + if (prevLogPath != null) { + log = new File(prevLogPath); + br = new BufferedReader(new FileReader(prevLogPath)); + return; + } + String logName = FILE_PREFIX + new SimpleDateFormat(DATE_FORMAT).format(new Date()); + log = new File(System.getProperty(TMP_DIR_PROPERTY), logName); + } + + public void create() throws IOException { + log.createNewFile(); + } + + public boolean isInitialized() { + return log.exists(); + } + + public void append(String[] input) throws IOException { + String line = String.join(" ", input) + "\n"; + Files.write(Paths.get(log.getAbsolutePath()), line.getBytes(), StandardOpenOption.APPEND); + } + + /** + * restore tries to recover the session from this SessionLog and apply it to the provided SimulationManager. + * @param SimulationManager simulationManager + * @param SessionLog newLog + * @throws IOException if reading the previous session log or writing to the new session log fails. + */ + public void restore(SimulationManager simulationManager, SessionLog newLog) throws IOException { + for (String line = br.readLine(); line != null; line = br.readLine()) { + String[] input = line.split(WHITESPACE_REGEX); + Command command = CommandRegistry.commandForString(input[0]); + command.execute(input, simulationManager); + if (newLog.isInitialized()) { + newLog.append(input); + } + } + } +} diff --git a/src/simulation/ConstraintManager.java b/src/simulation/ConstraintManager.java new file mode 100644 index 0000000..d04eafb --- /dev/null +++ b/src/simulation/ConstraintManager.java @@ -0,0 +1,47 @@ +package simulation; + +import java.util.ArrayList; +import java.util.List; +import java.util.HashMap; +import java.util.Map; + +/** + * ConstraintManager manages constraints to be applied to a model when traversing its states. + */ +public class ConstraintManager { + private Map constraints; + private int nextConstraintID; + private final static String NUM_HEADER = "Num"; + private final static String CONSTRAINT_HEADER = "Constraint"; + + public ConstraintManager() { + constraints = new HashMap<>(); + nextConstraintID = 1; + } + + public void addConstraint(String constraint) { + constraints.put(nextConstraintID, constraint); + nextConstraintID++; + } + + public boolean removeConstraint(int constraintID) { + return constraints.remove(constraintID) != null; + } + + public void clearConstraints() { + constraints.clear(); + } + + public List getConstraints() { + return new ArrayList(constraints.values()); + } + + public String getFormattedConstraints() { + StringBuilder sb = new StringBuilder(); + sb.append(String.format("\n%-8s%s\n", NUM_HEADER, CONSTRAINT_HEADER)); + for (int ID : constraints.keySet()) { + sb.append(String.format("%-8d%s\n", ID, constraints.get(ID))); + } + return sb.toString(); + } +} diff --git a/src/simulation/SimulationManager.java b/src/simulation/SimulationManager.java new file mode 100644 index 0000000..60377a7 --- /dev/null +++ b/src/simulation/SimulationManager.java @@ -0,0 +1,517 @@ +package simulation; + +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 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.File; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.HashMap; +import java.util.List; +import java.util.Map; +import java.util.Stack; + +import org.yaml.snakeyaml.error.YAMLException; + +public class SimulationManager { + private File alloyModelFile; + private String alloyModelString; + private String alloyInitString; + private Map> scopes; + private ParsingConf persistentParsingConf; // Set by setconf - 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 ConstraintManager constraintManager; + + private boolean traceMode; + + public SimulationManager() { + scopes = new HashMap<>(); + statePath = new StatePath(); + stateGraph = new StateGraph(); + persistentParsingConf = new ParsingConf(); + embeddedParsingConf = null; + activeSolutions = new Stack<>(); + constraintManager = new ConstraintManager(); + + traceMode = false; + } + + public boolean isTrace() { + return traceMode; + } + + /** + * 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; + } + + public boolean initializeWithModel(File model) { + if (AlloyInterface.compile(model.getPath()) == null) { + System.out.println("error. Could not parse model."); + return false; + } + + String modelString; + try { + modelString = AlloyUtils.readFromFile(model); + } catch (IOException e) { + System.out.println("error. Failed to read file."); + return false; + } + + String configString = ParsingConf.getConfStringFromFileString(modelString).trim(); + if (configString.isEmpty()) { + // If the new model has no embedded ParsingConf, make sure any existing embedded + // ParsingConf for the previous model is removed. + embeddedParsingConf = null; + } else { + try { + embeddedParsingConf = ParsingConf.initializeWithYaml(configString); + } catch (YAMLException e) { + System.out.println("error. Invalid configuration."); + 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.alloyModelFile = model; + 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, + false + ), + alloyModelFile + ); + } catch (IOException e) { + System.out.println("error. I/O failed, cannot initialize model."); + return false; + } + + CompModule compModule = AlloyInterface.compile(model.getAbsolutePath()); + if (compModule == null) { + System.out.println("error. Could not parse model."); + return false; + } + + A4Solution sol = AlloyInterface.run(compModule); + + 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 initialNodes = getStateNodesForA4Solution(sol); + statePath.initWithPath(initialNodes); + stateGraph.initWithNodes(initialNodes); + + this.traceMode = false; + this.activeSolutions.clear(); + + return true; + } + + public boolean initializeWithTrace(File trace) { + A4Solution sol; + try { + sol = AlloyInterface.solutionFromXMLFile(trace); + } catch (Exception e) { + return false; + } + + List stateNodes = getStateNodesForA4Solution(sol); + if (stateNodes.isEmpty()) { + return false; + } + + statePath.initWithPath(stateNodes); + statePath.setPosition(0); + stateGraph.initWithNodes(stateNodes); + + this.traceMode = true; + this.activeSolutions.clear(); + + return true; + } + + /** + * 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); + + // Decrement the position by (steps + 1) and then, if we're not past the beginning, + // step forward by 1, resulting in overall decrementing by (steps). It is done this way + // because the forward step gives us the A4Solution for a node, simplifyng the implementation + // for the `alt` command. + statePath.decrementPosition(steps + 1, traceMode); + if (initialPos <= steps) { + return; + } + 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); + } + } + + /** + * performStep steps the transition system forward by `steps` state transitions. + * @param steps + */ + public void performStep(int steps) { + if (isTrace()) { + statePath.incrementPosition(steps); + return; + } + + statePath.commitNodes(); + + try { + String curInitString; + if (stateGraph.size() > 1) { + curInitString = statePath.getCurNode().getAlloyInitString(); + } else { + curInitString = alloyInitString; + } + AlloyUtils.writeToFile( + AlloyUtils.annotatedTransitionSystem(alloyModelString + curInitString, getParsingConf(), steps, false), + alloyModelFile + ); + } catch (IOException e) { + System.out.println("Cannot perform step. I/O failed."); + return; + } + + CompModule compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + if (compModule == null) { + System.out.println("Cannot perform step. Could not parse model."); + return; + } + + A4Solution sol = AlloyInterface.run(compModule); + if (sol == null || !sol.satisfiable()) { + System.out.println("Cannot perform step. Transition constraint is unsatisfiable."); + } + + 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); + } + + 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); + + // Filter out the initial node to avoid re-adding it to statePath. + stateNodes.remove(0); + + statePath.clearTempPath(); + StateNode startNode = statePath.getCurNode(); + statePath.setTempPath(stateNodes); + + stateGraph.addNodes(startNode, stateNodes); + + 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.annotatedTransitionSystem(alloyModelString + curInitString + breakPredicate, getParsingConf(), steps, true), + alloyModelFile + ); + } catch (IOException e) { + return false; + } + + CompModule compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + if (compModule == null) { + return false; + } + + A4Solution sol = AlloyInterface.run(compModule); + if (sol == null) { + return false; + } else 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); + + return true; + } + + return false; + } + + /** + * 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; + } + + CompModule compModule = AlloyInterface.compile(alloyModelFile.getAbsolutePath()); + if (compModule == null) { + 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 getCurrentStateString() { + return statePath.getCurNode().toString(); + } + + public String getCurrentStateStringForProperty(String property) { + return statePath.getCurNode().stringForProperty(property); + } + + public String getCurrentStateDiffString() { + return statePath.getCurNode().getDiffString(statePath.getPrevNode()); + } + + public ConstraintManager getConstraintManager() { + return constraintManager; + } + + public String getWorkingDirPath() { + return System.getProperty("user.dir"); + } + + 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/state/StateGraph.java b/src/state/StateGraph.java new file mode 100644 index 0000000..836e615 --- /dev/null +++ b/src/state/StateGraph.java @@ -0,0 +1,103 @@ +package state; + +import java.util.ArrayList; +import java.util.List; + +/** + * StateGraph represents a directed graph containing all states visited in the active simulation. + */ +public class StateGraph { + private List nodes; + + public StateGraph() { + nodes = new ArrayList<>(); + } + + /** + * initWithNodes initializes the graph with initial nodes. + * @param List nodes + */ + public void initWithNodes(List nodes) { + this.nodes.clear(); + + for (int i = 0; i < nodes.size(); i++) { + StateNode node = nodes.get(i); + addNode(node); + + if (i > 0) { + StateNode prevNode = nodes.get(i - 1); + prevNode.addStep(node); + } + } + } + + /** + * addNodes adds a list of nodes to the graph, beginning at a start node. + * @param StateNode startNode + * @param List nodes + */ + public void addNodes(StateNode startNode, List nodes) { + // For every new node added, if it has the same state as an existing + // node, then add an outgoing edge from the current node to it, otherwise + // add it to the nodes list and then add the edge. Set the current node + // to the one we transitioned to. + StateNode curNode = getExistingNode(startNode); + for (StateNode node : nodes) { + StateNode nextNode = getExistingNode(node); + if (nextNode == null) { + nextNode = node; + addNode(nextNode); + } + + if (!curNode.getSteps().contains(nextNode)) { + curNode.addStep(nextNode); + } + + curNode = nextNode; + } + } + + public int size() { + return nodes.size(); + } + + /** + * getDOTString returns a DOT (graph description language) representation of the graph. + * @return String + */ + public String getDOTString() { + StringBuilder sb = new StringBuilder(); + + sb.append("digraph graphname {\n"); + for (StateNode node : nodes) { + List steps = node.getSteps(); + + if (steps.isEmpty()) { + sb.append(String.format("\tS%d\n", node.getIdentifier())); + continue; + } + + for (StateNode stepNode : steps) { + sb.append(String.format("\tS%d -> S%d\n", node.getIdentifier(), stepNode.getIdentifier())); + } + } + + sb.append("}\n"); + return sb.toString(); + } + + private void addNode(StateNode node) { + nodes.add(node); + node.setIdentifier(size()); + } + + private StateNode getExistingNode(StateNode node) { + for (StateNode existingNode : this.nodes) { + if (existingNode.equals(node)) { + return existingNode; + } + } + + return null; + } +} diff --git a/src/state/StateNode.java b/src/state/StateNode.java new file mode 100644 index 0000000..80e3f8a --- /dev/null +++ b/src/state/StateNode.java @@ -0,0 +1,197 @@ +package state; + +import alloy.AlloyConstants; +import alloy.AlloyUtils; +import alloy.ParsingConf; +import alloy.SigData; + +import java.util.ArrayList; +import java.util.Collections; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +/** + * 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 Map> state; // the state that this node represents + private int id; + private ParsingConf parsingConf; + private SigData sigData; + + public StateNode(SigData data, ParsingConf conf) { + sigData = data; + parsingConf = conf; + steps = new ArrayList<>(); + state = new HashMap<>(); + + for (String field : sigData.getFields()) { + state.put(field, new ArrayList<>()); + } + } + + public void addValueToField(String field, String value) { + if (!state.containsKey(field)) { + return; + } + + // Ensure values are sorted upon insertion. For the following reasons: + // 1. For user display. + // 2. Enables comparison between StateNodes. + List valuesForField = state.get(field); + for (int i = 0; i < valuesForField.size(); i++) { + if (value.compareTo(valuesForField.get(i)) > 0) { + continue; + } + + valuesForField.add(i, value); + return; + } + + valuesForField.add(value); + } + + public List getSteps() { + return steps; + } + + public void addStep(StateNode node) { + steps.add(node); + } + + @Override + public String toString() { + StringBuilder sb = new StringBuilder(); + for (String key : state.keySet()) { + sb.append(String.format("\n%s: %s ", key, AlloyConstants.BLOCK_INITIALIZER)); + sb.append(String.format("%s %s", String.join(", ", state.get(key)), AlloyConstants.BLOCK_TERMINATOR)); + } + sb.append("\n"); + return sb.toString(); + } + + public String stringForProperty(String property) { + if (!state.containsKey(property)) { + return "Property not found."; + } + + StringBuilder sb = new StringBuilder(); + sb.append("\n"); + for (String value : state.get(property)) { + sb.append(String.format("%s\n", value)); + } + return sb.toString(); + } + + /** + * @param StateNode other + * @return String representation of this, containing fields that are not equal to fields in other + */ + public String getDiffString(StateNode other) { + if (other == null) { + return toString(); + } + + Map> otherState = other.state; + + StringBuilder sb = new StringBuilder(); + for (String key : state.keySet()) { + if (!otherState.containsKey(key)) { + continue; + } + + List thisKeyContents = state.get(key); + List otherKeyContents = otherState.get(key); + + if (thisKeyContents.equals(otherKeyContents)) { + continue; + } + + sb.append(String.format("\n%s: %s ", key, AlloyConstants.BLOCK_INITIALIZER)); + sb.append(String.format("%s %s", String.join(", ", state.get(key)), AlloyConstants.BLOCK_TERMINATOR)); + } + sb.append("\n"); + return sb.toString(); + } + + /** + * Two StateNodes are considered to be equivalent if they represent the exact same state. + * @param other + * @return true if this is the same as other, else false + */ + @Override + public boolean equals(Object other) { + if (other == null) { + return false; + } + final StateNode otherNode = (StateNode) other; + if (!state.keySet().equals(otherNode.state.keySet())) { + return false; + } + for (String key : state.keySet()) { + List vals = state.get(key); + List otherVals = otherNode.state.get(key); + if (vals == null && otherVals != null) { + return false; + } + if (otherVals == null && vals != null) { + return false; + } + if (vals == null) { + break; + } + Collections.sort(vals); + Collections.sort(otherVals); + if (!vals.equals(otherVals)) { + return false; + } + } + return true; + } + + /** + * Generate an init predicate representing this instance's state in proper Alloy syntax. + * @return String representation of the state in correct Alloy model syntax + */ + public String getAlloyInitString() { + StringBuilder sb = new StringBuilder(); + for (Map.Entry> entry : state.entrySet()) { + List vals = entry.getValue(); + StringBuilder alloyFormattedValsBuilder = new StringBuilder(); + String prefix = ""; + for (String val : vals) { + alloyFormattedValsBuilder.append(prefix); + prefix = String.format(" %s ", AlloyConstants.PLUS); + String[] values = val.split(AlloyConstants.SET_DELIMITER); + alloyFormattedValsBuilder.append(values[0]); + for (int i = 1; i < values.length; i++) { + alloyFormattedValsBuilder.append(AlloyConstants.SET_DELIMITER); + alloyFormattedValsBuilder.append(values[i]); + } + } + + String value = (alloyFormattedValsBuilder.length() == 0) ? + AlloyUtils.getEmptyRelation(sigData.getArityForField(entry.getKey())) : + alloyFormattedValsBuilder.toString(); + sb.append( + String.format( + "\ts.%s = %s\n", + entry.getKey(), + value + ) + ); + } + + return AlloyUtils.makeStatePredicate(parsingConf.getInitPredicateName(), parsingConf.getStateSigName(), sb.toString()); + } + + public int getIdentifier() { + return id; + } + + public void setIdentifier(int id) { + this.id = id; + } +} diff --git a/src/state/StatePath.java b/src/state/StatePath.java new file mode 100644 index 0000000..8c6b185 --- /dev/null +++ b/src/state/StatePath.java @@ -0,0 +1,112 @@ +package state; + +import java.util.ArrayList; +import java.util.List; + +/** + * StatePath represents the path of nodes visited in the active model. + */ +public class StatePath { + private List path; + int tempPathSize; + private StateNode prev; + private int position; + + public StatePath() { + path = new ArrayList<>(); + position = 0; + tempPathSize = 0; + } + + private void appendPath(List path) { + this.path.addAll(path); + position = this.path.size() - 1; + } + + public void initWithPath(List path) { + this.path.clear(); + tempPathSize = 0; + appendPath(path); + } + + public boolean isEmpty() { + return path.isEmpty(); + } + + public StateNode getNode(int pos) { + if (pos < 0 || pos >= path.size()) { + return null; + } + return path.get(pos); + } + + public StateNode getCurNode() { + return path.isEmpty() ? null : path.get(position); + } + + public StateNode getPrevNode() { + return prev; + } + + public void setPosition(int position) { + prev = getCurNode(); + this.position = position; + } + + public int getPosition() { + return position; + } + + public void incrementPosition(int steps) { + setPosition(position + steps); + } + + public void decrementPosition(int steps, boolean traceMode) { + int newPos = position < steps ? 0 : position - steps; + setPosition(newPos); + if (position == 0) { + prev = null; + } else { + prev = path.get(position - 1); + } + if (traceMode) { + return; + } + path = path.subList(0, newPos + 1); + } + + public void commitNodes() { + tempPathSize = 0; + } + + public void setTempPath(List tempPath) { + clearTempPath(); + tempPathSize = tempPath.size(); + appendPath(tempPath); + } + + public void clearTempPath() { + position -= tempPathSize; + for (int i = 0; i < tempPathSize; i++) { + path.remove(path.size() - 1); + } + + tempPathSize = 0; + } + + public String getHistory(int n, boolean traceMode) { + int i = position - 1; + int j = i; + StringBuilder sb = new StringBuilder(); + while (j >= 0 && i - j < n) { + if (traceMode && j != 0) { + sb.insert(0, path.get(j).getDiffString(path.get(j - 1))); + } else { + sb.insert(0, path.get(j).toString()); + } + sb.insert(0, String.format("\n(-%d)\n----", i - j + 1)); + j--; + } + return sb.toString(); + } +} diff --git a/test/alloy/TestAlloyInterface.java b/test/alloy/TestAlloyInterface.java new file mode 100644 index 0000000..2d3d923 --- /dev/null +++ b/test/alloy/TestAlloyInterface.java @@ -0,0 +1,193 @@ +package alloy; + +import edu.mit.csail.sdg.ast.Sig; +import edu.mit.csail.sdg.translator.A4Solution; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Rule; +import org.junit.rules.TemporaryFolder; +import org.junit.Test; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.StandardOpenOption; +import java.util.HashMap; +import java.util.Map; + +public class TestAlloyInterface { + @Rule + public TemporaryFolder tempFolder = new TemporaryFolder(); + + @Test + public void testCompile() throws IOException { + File model = createModelForTesting(); + assertNotNull(AlloyInterface.compile(model.getPath())); + } + + @Test + public void testCompile_failureSyntax() throws IOException { + File model = createModelForTesting(); + + // Append invalid Alloy code to file. + String invalidCode = "}{"; + appendToFile(model, invalidCode); + + assertNull(AlloyInterface.compile(model.getPath())); + } + + @Test + public void testCompile_failureNoFile() throws IOException { + assertNull(AlloyInterface.compile("non-existant-file")); + } + + @Test + public void testRun() throws IOException { + File model = createModelForTesting(); + String runCommand = "run {} for 2 State"; + appendToFile(model, runCommand); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(model.getPath())); + assertNotNull(sol); + + Sig sig = AlloyInterface.getSigFromA4Solution(sol, "State"); + assertEquals(2, sol.eval(sig).size()); + } + + @Test + public void testRun_noCommands() throws IOException { + File model = createModelForTesting(); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(model.getPath())); + // Models contain a default command: 'Run Default for 4 but 4 int, 4 seq expect 0'. + assertNotNull(sol); + + Sig sig = AlloyInterface.getSigFromA4Solution(sol, "State"); + assertEquals(4, sol.eval(sig).size()); + } + + @Test + public void testRun_multipleCommands() throws IOException { + File model = createModelForTesting(); + String runCommands = String.join("\n", + "run {} for 3 State", + "run {} for 2 State" + ); + appendToFile(model, runCommands); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(model.getPath())); + assertNotNull(sol); + + // Only the last command should have run. + Sig sig = AlloyInterface.getSigFromA4Solution(sol, "State"); + assertEquals(2, sol.eval(sig).size()); + } + + @Test + public void testSolutionFromXMLFile() throws Exception { + File model = createModelForTesting(); + String runCommand = "run {} for 3 State"; + appendToFile(model, runCommand); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(model.getPath())); + assertNotNull(sol); + + Sig sig = AlloyInterface.getSigFromA4Solution(sol, "State"); + assertEquals(3, sol.eval(sig).size()); + + File xmlFile = tempFolder.newFile("test.xml"); + Map sources = new HashMap(); + sources.put(model.getPath(), new String(Files.readAllBytes(model.toPath()))); + sol.writeXML(xmlFile.getPath(), null, sources); + A4Solution solFromXML = AlloyInterface.solutionFromXMLFile(xmlFile); + + sig = AlloyInterface.getSigFromA4Solution(solFromXML, "State"); + assertEquals(3, solFromXML.eval(sig).size()); + } + + @Test + public void testSolutionFromXMLFile_invalidXML() throws IOException { + File xmlFile = tempFolder.newFile("test.xml"); + + appendToFile(xmlFile, "><"); + assertThrows(Exception.class, () -> { + AlloyInterface.solutionFromXMLFile(xmlFile); + }); + } + + @Test + public void testSolutionFromXMLFile_noFile() throws IOException { + assertThrows(Exception.class, () -> { + AlloyInterface.solutionFromXMLFile(null); + }); + } + + @Test + public void testSolutionFromXMLFile_validXMLInvalidStructure() throws IOException { + File xmlFile = tempFolder.newFile("test.xml"); + + appendToFile(xmlFile, ""); + assertThrows(Exception.class, () -> { + AlloyInterface.solutionFromXMLFile(xmlFile); + }); + } + + @Test + public void testGetSigFromA4Solution() throws IOException { + File model = createModelForTesting(); + String runCommand = "run {} for 2 State"; + appendToFile(model, runCommand); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(model.getPath())); + Sig sig = AlloyInterface.getSigFromA4Solution(sol, "State"); + assertNotNull(sig); + } + + @Test + public void testGetSigFromA4Solution_sigNotFound() throws IOException { + File model = createModelForTesting(); + String runCommand = "run {} for 2 State"; + appendToFile(model, runCommand); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(model.getPath())); + Sig sig = AlloyInterface.getSigFromA4Solution(sol, "Sig"); + assertNull(sig); + } + + private File createModelForTesting() throws IOException { + String modelString = String.join("\n", + "open util/ordering[State]", + "", + "abstract sig SwitchState {}", + "", + "one sig On, Off extends SwitchState {}", + "", + "sig State {", + " switch: SwitchState", + "}", + "", + "pred init[s: State] {", + " s.switch = Off", + "}", + "", + "pred next[s, s': State] {", + " s.switch = On implies s'.switch = Off", + " s.switch = Off implies s'.switch = On", + "}", + "", + "fact { init[first] }", + "", + "fact { all s: State, s': s.next { next[s, s'] } }", + "" + ); + + File tempFile = tempFolder.newFile("test.als"); + Files.write(tempFile.toPath(), modelString.getBytes()); + return tempFile; + } + + private void appendToFile(File file, String string) throws IOException { + Files.write(file.toPath(), string.getBytes(), StandardOpenOption.APPEND); + } +} diff --git a/test/alloy/TestAlloyUtils.java b/test/alloy/TestAlloyUtils.java new file mode 100644 index 0000000..0b78c79 --- /dev/null +++ b/test/alloy/TestAlloyUtils.java @@ -0,0 +1,206 @@ +package alloy; + +import edu.mit.csail.sdg.ast.Sig; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +import java.io.IOException; +import java.io.File; +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.TreeMap; + +public class TestAlloyUtils { + @Test + public void testGetEmptyRelation() { + String expected = "none -> none -> none"; + assertEquals(expected, AlloyUtils.getEmptyRelation(3)); + } + + @Test + public void testGetEmptyRelation_zero() { + String expected = "none"; + assertEquals(expected, AlloyUtils.getEmptyRelation(0)); + } + + @Test + public void testGetEmptyRelation_negative() { + String expected = "none"; + assertEquals(expected, AlloyUtils.getEmptyRelation(-3)); + } + + @Test + public void testAnnotatedTransitionSystem_untilFalse() { + String model = "Some model"; + int steps = 5; + boolean until = false; + String expected = String.join("\n", + "open util/ordering[State]", + "", + "Some model", + "", + "fact { init[first] }", + "", + "fact { all s: State, s': s.next { next[s, s'] } }", + "", + "run {} for exactly 6 State" + ); + String result = AlloyUtils.annotatedTransitionSystem( + model, + new ParsingConf(), + steps, + until + ); + assertEquals(expected, result); + } + + @Test + public void testAnnotatedTransitionSystem_untilTrue() { + String model = "Some model"; + int steps = 5; + boolean until = true; + String expected = String.join("\n", + "open util/ordering[State]", + "", + "Some model", + "", + "fact { init[first] }", + "", + "fact { all s: State, s': s.next { next[s, s'] } }", + "", + "run {break[last]} for exactly 6 State" + ); + String result = AlloyUtils.annotatedTransitionSystem( + model, + new ParsingConf(), + steps, + until + ); + assertEquals(expected, result); + } + + @Test + public void testGetBreakPredicate() { + List rawConstraints = new ArrayList(); + rawConstraints.add("f"); + rawConstraints.add("f=g"); + SigData sigData = new SigData(createNewSig()); + String expected = String.join("\n", + "", + "pred break[s: A] {", + "\t(s.f) or (s.f=s.g)", + "}", + "" + ); + assertEquals(expected, AlloyUtils.getBreakPredicate(rawConstraints, sigData)); + } + + @Test + public void testGetBreakPredicate_noConstraints() { + List rawConstraints = new ArrayList(); + SigData sigData = new SigData(createNewSig()); + String expected = String.join("\n", + "", + "pred break[s: A] {", + "\t", + "}", + "" + ); + assertEquals(expected, AlloyUtils.getBreakPredicate(rawConstraints, sigData)); + } + + @Test + public void testMakeStatePredicate() { + String predicateName = "test"; + String stateSigName = "State"; + String contents = "...\n"; + String expected = String.join("\n", + "", + "pred test[s: State] {", + "...", + "}", + "" + ); + assertEquals(expected, AlloyUtils.makeStatePredicate(predicateName, stateSigName, contents)); + } + + @Test + public void testGetConcreteSigsDefinition() { + Map sigScopes = new TreeMap(); + sigScopes.put("Player", 4); + sigScopes.put("Chair", 3); + + String expected = String.join("\n", + "one sig Chair_0, Chair_1, Chair_2 extends Chair {}", + "one sig Player_0, Player_1, Player_2, Player_3 extends Player {}", + "" + ); + assertEquals(expected, AlloyUtils.getConcreteSigsDefinition(sigScopes)); + } + + @Test + public void testGetConcreteSigsDefinition_someZero() { + Map sigScopes = new TreeMap(); + sigScopes.put("Player", 0); + sigScopes.put("Chair", 3); + + String expected = String.join("\n", + "one sig Chair_0, Chair_1, Chair_2 extends Chair {}", + "" + ); + assertEquals(expected, AlloyUtils.getConcreteSigsDefinition(sigScopes)); + } + + @Test + public void testGetConcreteSigsDefinition_allZero() { + Map sigScopes = new TreeMap(); + sigScopes.put("Player", 0); + sigScopes.put("Chair", 0); + + String expected = ""; + assertEquals(expected, AlloyUtils.getConcreteSigsDefinition(sigScopes)); + } + + @Test + public void testGetConcreteSigsDefinition_empty() { + Map sigScopes = new TreeMap(); + + String expected = ""; + assertEquals(expected, AlloyUtils.getConcreteSigsDefinition(sigScopes)); + } + + @Test + public void testCreateTmpFile() throws IOException { + File file = new File("/tmp/sample.als"); + String contents = "Hello World"; + file.createNewFile(); + File tmpFile = AlloyUtils.createTmpFile(contents, file); + assertTrue(tmpFile.exists()); + assertEquals("_tmp_" + file.getName(), tmpFile.getName()); + assertEquals(file.getParent(), tmpFile.getParent()); + file.delete(); + } + + @Test + public void testCreateTmpFile_nullParentPath() throws IOException { + File file = new File("sample.als"); + String contents = "Hello World"; + file.createNewFile(); + File tmpFile = AlloyUtils.createTmpFile(contents, file); + assertTrue(tmpFile.exists()); + assertEquals("_tmp_" + file.getName(), tmpFile.getName()); + assertEquals(file.getParent(), tmpFile.getParent()); + file.delete(); + } + + private Sig createNewSig() { + Sig sigA = new Sig.PrimSig("A"); + Sig sigB = new Sig.PrimSig("B"); + Sig.Field f1 = sigA.addField("f", sigB.lone_arrow_lone(sigB)); + Sig.Field f2 = sigA.addField("g", sigB); + return sigA; + } +} diff --git a/test/alloy/TestParsingConf.java b/test/alloy/TestParsingConf.java new file mode 100644 index 0000000..0859cd8 --- /dev/null +++ b/test/alloy/TestParsingConf.java @@ -0,0 +1,59 @@ +package alloy; + +import alloy.ParsingConf; + +import java.util.Map; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +public class TestParsingConf { + @Test + public void testGetConfStringFromFileString() { + String content = String.join("\n", + "/* BEGIN_ALDB_CONF", + " * transitionRelationName: trans", + " * END_ALDB_CONF", + " */", + "some alloy model here" + ); + String result = "transitionRelationName: trans"; + String confString = ParsingConf.getConfStringFromFileString(content).trim(); + assertEquals(result, confString); + } + + @Test + public void testGetConfStringFromFileString_invalidConf() { + String content = String.join("\n", + "/* BEGIN_ALDB_CONF", + " * transitionRelationName: trans", + " */", + "some alloy model here" + ); + String result = ""; + String confString = ParsingConf.getConfStringFromFileString(content).trim(); + assertEquals(result, confString); + } + + @Test + public void testInitializeWithYaml() { + String content = String.join("\n", + "stateSigName: name", + "initPredicateName: init", + "transitionRelationName: trans", + "additionalSigScopes:", + " Chair: 1", + " Player: 2" + ); + ParsingConf pc = ParsingConf.initializeWithYaml(content); + Map ass = pc.getAdditionalSigScopes(); + assertTrue(ass.containsKey("Chair")); + assertTrue(ass.containsKey("Player")); + assertEquals(1, ass.get("Chair")); + assertEquals(2, ass.get("Player")); + assertEquals("name", pc.getStateSigName()); + assertEquals("init", pc.getInitPredicateName()); + assertEquals("trans", pc.getTransitionRelationName()); + } +} diff --git a/test/alloy/TestSigData.java b/test/alloy/TestSigData.java new file mode 100644 index 0000000..aa66592 --- /dev/null +++ b/test/alloy/TestSigData.java @@ -0,0 +1,51 @@ +package alloy; + +import alloy.SigData; + +import edu.mit.csail.sdg.ast.Sig; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Before; +import org.junit.Test; + +import java.util.HashSet; +import java.util.Set; + +public class TestSigData { + private SigData sigData; + + @Before + public void init() { + Sig sigA = new Sig.PrimSig("A"); + Sig sigB = new Sig.PrimSig("B"); + Sig.Field f1 = sigA.addField("f", sigB.lone_arrow_lone(sigB)); + Sig.Field f2 = sigA.addField("g", sigB); + sigData = new SigData(sigA); + } + + @Test + public void testGetLabel() { + assertEquals("A", sigData.getLabel()); + } + + @Test + public void testGetFields() { + Set expected = new HashSet<>(); + expected.add("f"); + expected.add("g"); + assertEquals(expected, sigData.getFields()); + } + + @Test + public void testGetTypeForField() { + assertEquals("{A->B->B}", sigData.getTypeForField("f")); + assertEquals("{A->B}", sigData.getTypeForField("g")); + } + + @Test + public void testGetArityForField() { + assertEquals(2, sigData.getArityForField("f")); + assertEquals(1, sigData.getArityForField("g")); + } +} diff --git a/test/commands/TestAltCommand.java b/test/commands/TestAltCommand.java new file mode 100644 index 0000000..2126f35 --- /dev/null +++ b/test/commands/TestAltCommand.java @@ -0,0 +1,88 @@ +package commands; + +import commands.AltCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestAltCommand extends TestCommand { + private final AltCommand alt = new AltCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(alt.getName(), CommandConstants.ALT_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(alt.getDescription(), CommandConstants.ALT_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(alt.getHelp(), CommandConstants.ALT_HELP); + } + + @Test + public void testGetShorthand() { + assertEquals(alt.getShorthand(), CommandConstants.ALT_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertFalse(alt.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + String res = "Response"; + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.selectAlternatePath(anyBoolean())).thenReturn(true); + when(simulationManager.getCurrentStateString()).thenReturn(res); + + String[] input = {"alt"}; + alt.execute(input, simulationManager); + verify(simulationManager).getCurrentStateString(); + assertEquals(res + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidInput() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"alt", "random"}; + String errMsg = CommandConstants.ALT_HELP + "\n"; + alt.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_noAlternatePaths() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.selectAlternatePath(anyBoolean())).thenReturn(false); + String[] input = {"alt", "-r"}; + String errMsg = CommandConstants.ALT_UNAVAILABLE + "\n"; + alt.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + + String[] input = {"alt"}; + alt.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestBreakCommand.java b/test/commands/TestBreakCommand.java new file mode 100644 index 0000000..1d34b70 --- /dev/null +++ b/test/commands/TestBreakCommand.java @@ -0,0 +1,152 @@ +package commands; + +import commands.BreakCommand; +import simulation.ConstraintManager; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestBreakCommand extends TestCommand { + private final BreakCommand breakCommand = new BreakCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + private final ConstraintManager cm = mock(ConstraintManager.class); + + @Test + public void testGetName() { + assertEquals(breakCommand.getName(), CommandConstants.BREAK_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(breakCommand.getDescription(), CommandConstants.BREAK_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(breakCommand.getHelp(), CommandConstants.BREAK_HELP); + } + + @Test + public void testGetShorthand() { + assertEquals(breakCommand.getShorthand(), CommandConstants.BREAK_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertFalse(breakCommand.requiresFile()); + } + + @Test + public void testExecute_rm() { + setupStreams(); + when(simulationManager.getConstraintManager()).thenReturn(cm); + when(cm.removeConstraint(anyInt())).thenReturn(true); + + String[] input = {"break", "-rm", "3"}; + breakCommand.execute(input, simulationManager); + verify(cm).removeConstraint(3); + restoreStreams(); + } + + @Test + public void testExecute_l() { + setupStreams(); + String res = "formatted constraint"; + when(simulationManager.getConstraintManager()).thenReturn(cm); + when(cm.getFormattedConstraints()).thenReturn(res); + + String[] input = {"break", "-l"}; + breakCommand.execute(input, simulationManager); + verify(cm).getFormattedConstraints(); + assertEquals(res + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_c() { + when(simulationManager.getConstraintManager()).thenReturn(cm); + String[] input = {"break", "-c"}; + breakCommand.execute(input, simulationManager); + verify(cm).clearConstraints(); + } + + @Test + public void testExecute_addConstraint() { + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getConstraintManager()).thenReturn(cm); + when(simulationManager.validateConstraint(anyString())).thenReturn(true); + + String[] input = {"break", "\"a = b\"", "c", "d=f"}; + breakCommand.execute(input, simulationManager); + verify(cm).addConstraint("a = b"); + verify(cm).addConstraint("c"); + verify(cm).addConstraint("d=f"); + } + + @Test + public void testExecute_help() { + setupStreams(); + String[] input = {"break"}; + String errMsg = CommandConstants.BREAK_HELP + "\n"; + breakCommand.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidInput_RM() { + setupStreams(); + String[] input = {"break", "-rm"}; + String errMsg = CommandConstants.BREAK_HELP + "\n"; + breakCommand.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidConstraintIDType() throws NumberFormatException { + setupStreams(); + String[] input = {"break", "-rm", "one"}; + String errMsg = CommandConstants.INTEGER_ERROR + "\n"; + breakCommand.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidConstraintID() { + setupStreams(); + when(simulationManager.getConstraintManager()).thenReturn(cm); + String[] input = {"break", "-rm", "99"}; + int constraintID = 99; + String errMsg = String.format(CommandConstants.INVALID_CONSTRAINT_ID, constraintID) + "\n"; + breakCommand.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidConstraint() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.validateConstraint(anyString())).thenReturn(false); + String[] input = {"break", "invalid"}; + String errMsg = String.format(CommandConstants.INVALID_CONSTRAINT, input[1]) + "\n"; + breakCommand.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + String[] input = {"break", "test"}; + breakCommand.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestCommand.java b/test/commands/TestCommand.java new file mode 100644 index 0000000..f34cd7e --- /dev/null +++ b/test/commands/TestCommand.java @@ -0,0 +1,36 @@ +package commands; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Ignore; +import org.junit.Rule; +import org.junit.rules.TemporaryFolder; + +import java.io.ByteArrayOutputStream; +import java.io.File; +import java.io.IOException; +import java.io.PrintStream; +import java.nio.file.Files; + +@Ignore("Base class for command testing") +public class TestCommand { + @Rule + public TemporaryFolder tempFolder = new TemporaryFolder(); + + protected final ByteArrayOutputStream outContent = new ByteArrayOutputStream(); + protected final PrintStream originalOut = System.out; + + protected void setupStreams() { + System.setOut(new PrintStream(outContent)); + } + + protected void restoreStreams() { + System.setOut(originalOut); + } + + protected File createFileWithContent(String content) throws IOException { + File file = tempFolder.newFile("test"); + Files.write(file.toPath(), content.getBytes()); + return file; + } +} diff --git a/test/commands/TestCurrentCommand.java b/test/commands/TestCurrentCommand.java new file mode 100644 index 0000000..80df669 --- /dev/null +++ b/test/commands/TestCurrentCommand.java @@ -0,0 +1,77 @@ +package commands; + +import commands.CurrentCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestCurrentCommand extends TestCommand { + private final CurrentCommand current = new CurrentCommand(); + SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(current.getName(), CommandConstants.CURRENT_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(current.getDescription(), CommandConstants.CURRENT_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(current.getHelp(), CommandConstants.CURRENT_HELP); + } + + @Test + public void testGetShorthand() { + assertEquals(current.getShorthand(), CommandConstants.CURRENT_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertFalse(current.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + String res = "curr state"; + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getCurrentStateString()).thenReturn(res); + + String[] input = {"c"}; + current.execute(input, simulationManager); + verify(simulationManager).getCurrentStateString(); + assertEquals(res + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_specificProperty() { + setupStreams(); + String res = "property response"; + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getCurrentStateStringForProperty(anyString())).thenReturn(res); + + String[] input = {"c", "property"}; + current.execute(input, simulationManager); + verify(simulationManager).getCurrentStateStringForProperty(input[1]); + assertEquals(res + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + String[] input = {"c", "0"}; + current.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestDotCommand.java b/test/commands/TestDotCommand.java new file mode 100644 index 0000000..e22de3a --- /dev/null +++ b/test/commands/TestDotCommand.java @@ -0,0 +1,74 @@ +package commands; + +import commands.DotCommand; +import commands.CommandConstants; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Rule; +import org.junit.rules.TemporaryFolder; +import org.junit.Test; + +import java.io.File; +import java.io.IOException; + +public class TestDotCommand extends TestCommand { + private final DotCommand dot = new DotCommand(); + SimulationManager simulationManager = mock(SimulationManager.class); + + @Rule + public TemporaryFolder tmpdir = new TemporaryFolder(); + + @Test + public void testGetName() { + assertEquals(dot.getName(), CommandConstants.DOT_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(dot.getDescription(), CommandConstants.DOT_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(dot.getHelp(), CommandConstants.DOT_HELP); + } + + @Test + public void testGetShorthand() { + assertEquals(dot.getShorthand(), CommandConstants.DOT_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertFalse(dot.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getWorkingDirPath()).thenReturn(tmpdir.getRoot().getAbsolutePath()); + when(simulationManager.getDOTString()).thenReturn("foo"); + + String[] input = {"dot"}; + dot.execute(input, simulationManager); + verify(simulationManager).getDOTString(); + assertTrue(outContent.toString().contains(CommandConstants.DONE)); + assertFalse(outContent.toString().contains(CommandConstants.IO_FAILED)); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + + String[] input = {"dot"}; + dot.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestEmptyCommand.java b/test/commands/TestEmptyCommand.java new file mode 100644 index 0000000..571632e --- /dev/null +++ b/test/commands/TestEmptyCommand.java @@ -0,0 +1,31 @@ +package commands; + +import commands.EmptyCommand; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +public class TestEmptyCommand { + private final EmptyCommand empty = new EmptyCommand(); + + @Test + public void testGetName() { + assertNull(empty.getName()); + } + + @Test + public void testGetDescription() { + assertNull(empty.getDescription()); + } + + @Test + public void testGetHelp() { + assertNull(empty.getHelp()); + } + + @Test + public void testRequiresFile() { + assertFalse(empty.requiresFile()); + } +} diff --git a/test/commands/TestHelpCommand.java b/test/commands/TestHelpCommand.java new file mode 100644 index 0000000..d709c3a --- /dev/null +++ b/test/commands/TestHelpCommand.java @@ -0,0 +1,94 @@ +package commands; + +import commands.HelpCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +public class TestHelpCommand extends TestCommand { + private final HelpCommand help = new HelpCommand(); + private final SimulationManager simulationManager = new SimulationManager(); + private final String help_all_commands = String.join("\n", + "Available commands:", + "", + "alt -- Select an alternate execution path", + "break -- Control the set of constraints used", + "current -- Display the current state", + "dot -- Dump DOT graph to disk", + "help -- Display the list of available commands", + "history -- Display past states", + "load -- Load an Alloy model", + "quit -- Exit ALDB", + "reverse-step -- Go back n steps in the current state traversal path", + "setconf -- Set parsing options for the current session", + "scope -- Display scope set", + "step -- Perform a state transition of n steps", + "trace -- Load a saved Alloy XML instance", + "until -- Run until constraints are met", + "", + "Type \"help\" followed by a command name for full documentation." + ); + + @Test + public void testGetName() { + assertEquals(help.getName(), CommandConstants.HELP_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(help.getDescription(), CommandConstants.HELP_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(help_all_commands, help.getHelp()); + } + + @Test + public void testGetShorthand() { + assertEquals(help.getShorthand(), CommandConstants.HELP_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertFalse(help.requiresFile()); + } + + @Test + public void testExecute_validCommands() { + setupStreams(); + String[] sampleCommands = {"step", "load", "break"}; + for (String cmd : sampleCommands) { + String[] input = {"help", cmd}; + help.execute(input, simulationManager); + } + String msg = String.join("\n", + CommandConstants.STEP_HELP, + CommandConstants.LOAD_HELP, + CommandConstants.BREAK_HELP + ); + assertEquals(msg + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidCommand() { + setupStreams(); + String invalidCommand = "invalid"; + String[] input = {"help", invalidCommand}; + help.execute(input, simulationManager); + assertEquals(help_all_commands + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_justHelp() { + setupStreams(); + String[] input = {"help"}; + help.execute(input, simulationManager); + assertEquals(help_all_commands + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestHistoryCommand.java b/test/commands/TestHistoryCommand.java new file mode 100644 index 0000000..5e6ade0 --- /dev/null +++ b/test/commands/TestHistoryCommand.java @@ -0,0 +1,78 @@ +package commands; + +import commands.HistoryCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestHistoryCommand extends TestCommand { + private final HistoryCommand history = new HistoryCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(history.getName(), CommandConstants.HISTORY_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(history.getDescription(), CommandConstants.HISTORY_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(history.getHelp(), CommandConstants.HISTORY_HELP); + } + + @Test + public void testRequiresFile() { + assertFalse(history.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + String response = "history"; + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getHistory(anyInt())).thenReturn(response); + String[] input = {"history", "5"}; + history.execute(input, simulationManager); + verify(simulationManager).getHistory(5); + assertEquals(response + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_lessThanOne() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"history", "0"}; + history.execute(input, simulationManager); + assertEquals(CommandConstants.GR_ONE_ERROR + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidInteger() throws NumberFormatException { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"history", "not_an_integer"}; + history.execute(input, simulationManager); + assertEquals(CommandConstants.INTEGER_ERROR + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + + String[] input = {"history"}; + history.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestLoadCommand.java b/test/commands/TestLoadCommand.java new file mode 100644 index 0000000..3800b50 --- /dev/null +++ b/test/commands/TestLoadCommand.java @@ -0,0 +1,92 @@ +package commands; + +import commands.LoadCommand; +import simulation.SimulationManager; + +import java.io.File; +import java.io.IOException; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestLoadCommand extends TestCommand { + private final LoadCommand load = new LoadCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(load.getName(), CommandConstants.LOAD_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(load.getDescription(), CommandConstants.LOAD_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(load.getHelp(), CommandConstants.LOAD_HELP); + } + + @Test + public void testGetShorthand() { + assertEquals(load.getShorthand(), CommandConstants.LOAD_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertTrue(load.requiresFile()); + } + + @Test + public void testExecute() throws IOException { + setupStreams(); + File file = createFileWithContent("content"); + when(simulationManager.initializeWithModel(any(File.class))).thenReturn(true); + + String[] input = {"load", file.getPath()}; + load.execute(input, simulationManager); + String msg = String.format(CommandConstants.READING_MODEL, input[1]); + msg += CommandConstants.DONE + "\n"; + assertEquals(msg, outContent.toString()); + verify(simulationManager).initializeWithModel(any(File.class)); + file.delete(); + restoreStreams(); + } + + @Test + public void testExecute_embeddedConf() throws IOException { + setupStreams(); + String content = String.join("\n", + "/* BEGIN_ALDB_CONF", + " * transitionRelationName: trans", + " * END_ALDB_CONF", + " */", + "some alloy model here" + ); + File file = createFileWithContent(content); + when(simulationManager.initializeWithModel(any(File.class))).thenReturn(true); + + String[] input = {"load", file.getPath()}; + load.execute(input, simulationManager); + String msg = String.format(CommandConstants.READING_MODEL, input[1]); + msg += CommandConstants.DONE + "\n"; + assertEquals(msg, outContent.toString()); + verify(simulationManager).initializeWithModel(any(File.class)); + file.delete(); + restoreStreams(); + } + + @Test + public void testExecute_noFile() { + setupStreams(); + String[] input = {"load", "no_file"}; + String errMsg = String.format(CommandConstants.NO_SUCH_FILE, input[1]); + load.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + verifyZeroInteractions(simulationManager); + restoreStreams(); + } +} diff --git a/test/commands/TestNotFoundCommand.java b/test/commands/TestNotFoundCommand.java new file mode 100644 index 0000000..a500986 --- /dev/null +++ b/test/commands/TestNotFoundCommand.java @@ -0,0 +1,43 @@ +package commands; + +import commands.NotFoundCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +public class TestNotFoundCommand extends TestCommand { + private final NotFoundCommand notFound = new NotFoundCommand(); + private final SimulationManager simulationManager = new SimulationManager(); + + @Test + public void testGetName() { + assertNull(notFound.getName()); + } + + @Test + public void testGetDescription() { + assertNull(notFound.getDescription()); + } + + @Test + public void testGetHelp() { + assertNull(notFound.getHelp()); + } + + @Test + public void testRequiresFile() { + assertFalse(notFound.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + String[] input = {"fydp"}; + String errMsg = String.format(CommandConstants.UNDEFINED_COMMAND, input[0]); + notFound.execute(input, simulationManager); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestQuitCommand.java b/test/commands/TestQuitCommand.java new file mode 100644 index 0000000..1268076 --- /dev/null +++ b/test/commands/TestQuitCommand.java @@ -0,0 +1,51 @@ +package commands; + +import commands.QuitCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Rule; +import org.junit.Test; +import org.junit.contrib.java.lang.system.ExpectedSystemExit; + +public class TestQuitCommand extends TestCommand { + private final QuitCommand quit = new QuitCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Rule + public final ExpectedSystemExit exit = ExpectedSystemExit.none(); + + @Test + public void testGetName() { + assertEquals(quit.getName(), CommandConstants.QUIT_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(quit.getDescription(), CommandConstants.QUIT_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(quit.getHelp(), CommandConstants.QUIT_HELP); + } + + @Test + public void testGetShorthand() { + assertEquals(quit.getShorthand(), CommandConstants.QUIT_SHORTHAND); + } + + @Test + public void testRequiresFile() { + assertFalse(quit.requiresFile()); + } + + @Test + public void testExecute() { + exit.expectSystemExitWithStatus(0); + String[] input = {"quit"}; + quit.execute(input, simulationManager); + } +} diff --git a/test/commands/TestReverseStepCommand.java b/test/commands/TestReverseStepCommand.java new file mode 100644 index 0000000..e018cd1 --- /dev/null +++ b/test/commands/TestReverseStepCommand.java @@ -0,0 +1,73 @@ +package commands; + +import commands.ReverseStepCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestReverseStepCommand extends TestCommand { + private final ReverseStepCommand reverseStep = new ReverseStepCommand(); + SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(reverseStep.getName(), CommandConstants.REVERSE_STEP_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(reverseStep.getDescription(), CommandConstants.REVERSE_STEP_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(reverseStep.getHelp(), CommandConstants.REVERSE_STEP_HELP); + } + + @Test + public void testRequiresFile() { + assertFalse(reverseStep.requiresFile()); + } + + @Test + public void testExecute() { + when(simulationManager.isInitialized()).thenReturn(true); + doNothing().when(simulationManager).performReverseStep(isA(Integer.class)); + String[] input = {"rs", "3"}; + reverseStep.execute(input, simulationManager); + verify(simulationManager).performReverseStep(3); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + String[] input = {"rs", "0"}; + reverseStep.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_lessThanOne() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"rs", "0"}; + reverseStep.execute(input, simulationManager); + assertEquals(CommandConstants.GR_ONE_ERROR + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidInteger() throws NumberFormatException { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"rs", "not_an_integer"}; + reverseStep.execute(input, simulationManager); + assertEquals(CommandConstants.INTEGER_ERROR + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestScopeCommand.java b/test/commands/TestScopeCommand.java new file mode 100644 index 0000000..90dfcaa --- /dev/null +++ b/test/commands/TestScopeCommand.java @@ -0,0 +1,88 @@ +package commands; + +import commands.ScopeCommand; +import simulation.SimulationManager; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.List; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestScopeCommand extends TestCommand { + private final ScopeCommand scope = new ScopeCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(scope.getName(), CommandConstants.SCOPE_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(scope.getDescription(), CommandConstants.SCOPE_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(scope.getHelp(), CommandConstants.SCOPE_HELP); + } + + @Test + public void testRequiresFile() { + assertFalse(scope.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + + String[] input = {"scope"}; + scope.execute(input, simulationManager); + verify(simulationManager).getScopes(); + restoreStreams(); + } + + @Test + public void testExecute_sigInput() { + setupStreams(); + List res = new ArrayList<>(); + res.add("scope"); + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getScopeForSig(anyString())).thenReturn(res); + + String[] input = {"scope", "sig"}; + scope.execute(input, simulationManager); + verify(simulationManager).getScopeForSig("sig"); + String msg = "\nscope\n\n"; + assertEquals(msg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidScope() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.getScopeForSig(anyString())).thenReturn(null); + String[] input = {"scope", "null"}; + scope.execute(input, simulationManager); + String errMsg = CommandConstants.SIG_NOT_FOUND + "\n"; + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + + String[] input = {"scope"}; + scope.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestSetConfCommand.java b/test/commands/TestSetConfCommand.java new file mode 100644 index 0000000..06d73ce --- /dev/null +++ b/test/commands/TestSetConfCommand.java @@ -0,0 +1,96 @@ +package commands; + +import alloy.ParsingConf; +import commands.SetConfCommand; +import simulation.SimulationManager; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; +import org.yaml.snakeyaml.error.YAMLException; + +public class TestSetConfCommand extends TestCommand { + private final SetConfCommand setConf = new SetConfCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(setConf.getName(), CommandConstants.SETCONF_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(setConf.getDescription(), CommandConstants.SETCONF_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(setConf.getHelp(), CommandConstants.SETCONF_HELP); + } + + @Test + public void testRequiresFile() { + assertTrue(setConf.requiresFile()); + } + + @Test + public void testExecute() throws IOException { + setupStreams(); + File file = createFileWithContent("transitionConstraintName: trans"); + doNothing().when(simulationManager).setParsingConf(isA(ParsingConf.class)); + + String[] input = {"setconf", file.getPath()}; + setConf.execute(input, simulationManager); + verify(simulationManager).setParsingConf(any(ParsingConf.class)); + String msg = String.format(CommandConstants.SETTING_PARSING_OPTIONS_FROM, input[1]); + msg += CommandConstants.DONE + "\n"; + assertEquals(msg, outContent.toString()); + file.delete(); + restoreStreams(); + } + + @Test + public void testExecute_setDefault() { + setupStreams(); + doNothing().when(simulationManager).setParsingConf(isA(ParsingConf.class)); + String[] input = {"setconf"}; + setConf.execute(input, simulationManager); + verify(simulationManager).setParsingConf(any(ParsingConf.class)); + String msg = CommandConstants.SETTING_PARSING_OPTIONS; + msg += CommandConstants.DONE + "\n"; + assertEquals(msg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidFile() throws IOException { + setupStreams(); + String[] input = {"setconf", "does_not_exist.txt"}; + setConf.execute(input, simulationManager); + String errMsg = String.format(CommandConstants.SETTING_PARSING_OPTIONS_FROM, input[1]); + errMsg += CommandConstants.FAILED_TO_READ_FILE + "\n"; + assertEquals(errMsg, outContent.toString()); + verifyZeroInteractions(simulationManager); + restoreStreams(); + } + + @Test + public void testExecute_invalidYaml() throws IOException, YAMLException { + setupStreams(); + File file = createFileWithContent("invalid yaml"); + + String[] input = {"setconf", file.getPath()}; + setConf.execute(input, simulationManager); + String errMsg = String.format(CommandConstants.SETTING_PARSING_OPTIONS_FROM, input[1]); + errMsg += CommandConstants.FAILED_TO_READ_CONF + "\n"; + assertEquals(errMsg, outContent.toString()); + verifyZeroInteractions(simulationManager); + file.delete(); + restoreStreams(); + } +} diff --git a/test/commands/TestStepCommand.java b/test/commands/TestStepCommand.java new file mode 100644 index 0000000..09b1ca1 --- /dev/null +++ b/test/commands/TestStepCommand.java @@ -0,0 +1,100 @@ +package commands; + +import commands.StepCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestStepCommand extends TestCommand { + private final StepCommand step = new StepCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(step.getName(), CommandConstants.STEP_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(step.getDescription(), CommandConstants.STEP_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(step.getHelp(), CommandConstants.STEP_HELP); + } + + @Test + public void testRequiresFile() { + assertFalse(step.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + String state = "state"; + when(simulationManager.isInitialized()).thenReturn(true); + doNothing().when(simulationManager).performStep(isA(Integer.class)); + when(simulationManager.getCurrentStateString()).thenReturn(state); + + String[] input = {"s", "3"}; + step.execute(input, simulationManager); + verify(simulationManager).performStep(3); + verify(simulationManager).getCurrentStateString(); + assertEquals(state + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_isTrace() { + setupStreams(); + String trace = "trace"; + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.isTrace()).thenReturn(true); + doNothing().when(simulationManager).performStep(isA(Integer.class)); + when(simulationManager.getCurrentStateDiffString()).thenReturn(trace); + + String[] input = {"s", "3"}; + step.execute(input, simulationManager); + verify(simulationManager).performStep(3); + verify(simulationManager).getCurrentStateDiffString(); + assertEquals(trace + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + + String[] input = {"s", "0"}; + step.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_lessThanOne() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + + String[] input = {"s", "0"}; + step.execute(input, simulationManager); + assertEquals(CommandConstants.GR_ONE_ERROR + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidInteger() throws NumberFormatException { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + + String[] input = {"s", "not_an_integer"}; + step.execute(input, simulationManager); + assertEquals(CommandConstants.INTEGER_ERROR + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/commands/TestTraceCommand.java b/test/commands/TestTraceCommand.java new file mode 100644 index 0000000..16954ce --- /dev/null +++ b/test/commands/TestTraceCommand.java @@ -0,0 +1,86 @@ +package commands; + +import commands.TraceCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; +import java.io.File; +import java.io.IOException; + +public class TestTraceCommand extends TestCommand { + private final TraceCommand trace = new TraceCommand(); + private final SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(trace.getName(), CommandConstants.TRACE_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(trace.getDescription(), CommandConstants.TRACE_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(trace.getHelp(), CommandConstants.TRACE_HELP); + } + + @Test + public void testRequiresFile() { + assertTrue(trace.requiresFile()); + } + + @Test + public void testExecute_invalidInputLength() { + setupStreams(); + String[] input = {"t"}; + trace.execute(input, simulationManager); + String errMsg = CommandConstants.NO_FILE_SPECIFIED + "\n"; + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidFile() { + setupStreams(); + String[] input = {"t", "does_not_exist.txt"}; + trace.execute(input, simulationManager); + String errMsg = String.format(CommandConstants.NO_SUCH_FILE, input[1]); + assertEquals(errMsg, outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute() throws IOException { + setupStreams(); + when(simulationManager.initializeWithTrace(any(File.class))).thenReturn(true); + File file = createFileWithContent(""); + + String[] input = {"t", file.getPath()}; + trace.execute(input, simulationManager); + String msg = String.format(CommandConstants.READING_TRACE, input[1]); + msg += CommandConstants.DONE + "\n"; + assertEquals(msg, outContent.toString()); + file.delete(); + restoreStreams(); + } + + @Test + public void testExecute_invalidTrace() throws IOException { + setupStreams(); + when(simulationManager.initializeWithTrace(any(File.class))).thenReturn(false); + File file = createFileWithContent(""); + + String[] input = {"t", file.getPath()}; + trace.execute(input, simulationManager); + String msg = String.format(CommandConstants.READING_TRACE, input[1]); + msg += CommandConstants.INVALID_TRACE + "\n"; + assertEquals(msg, outContent.toString()); + file.delete(); + restoreStreams(); + } +} diff --git a/test/commands/TestUntilCommand.java b/test/commands/TestUntilCommand.java new file mode 100644 index 0000000..54fa18b --- /dev/null +++ b/test/commands/TestUntilCommand.java @@ -0,0 +1,93 @@ +package commands; + +import commands.UntilCommand; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; +import static org.mockito.Mockito.*; + +import org.junit.Test; + +public class TestUntilCommand extends TestCommand { + private final UntilCommand until = new UntilCommand(); + SimulationManager simulationManager = mock(SimulationManager.class); + + @Test + public void testGetName() { + assertEquals(until.getName(), CommandConstants.UNTIL_NAME); + } + + @Test + public void testGetDescription() { + assertEquals(until.getDescription(), CommandConstants.UNTIL_DESCRIPTION); + } + + @Test + public void testGetHelp() { + assertEquals(until.getHelp(), CommandConstants.UNTIL_HELP); + } + + @Test + public void testRequiresFile() { + assertFalse(until.requiresFile()); + } + + @Test + public void testExecute() { + setupStreams(); + String curState = "Current state"; + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.performUntil(anyInt())).thenReturn(true); + when(simulationManager.getCurrentStateString()).thenReturn(curState); + + String[] input = {"u", "3"}; + until.execute(input, simulationManager); + verify(simulationManager).performUntil(3); + verify(simulationManager).getCurrentStateString(); + assertEquals(curState + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_failure() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + when(simulationManager.performUntil(anyInt())).thenReturn(false); + + String[] input = {"u", "3"}; + until.execute(input, simulationManager); + verify(simulationManager).performUntil(3); + assertEquals(CommandConstants.UNTIL_FAILED + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_uninitialized() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(false); + String[] input = {"u", "1"}; + until.execute(input, simulationManager); + assertEquals(CommandConstants.NO_MODEL_LOADED + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_lessThanOne() { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"u", "0"}; + until.execute(input, simulationManager); + assertEquals(CommandConstants.GR_ONE_ERROR + "\n", outContent.toString()); + restoreStreams(); + } + + @Test + public void testExecute_invalidInteger() throws NumberFormatException { + setupStreams(); + when(simulationManager.isInitialized()).thenReturn(true); + String[] input = {"u", "not_an_integer"}; + until.execute(input, simulationManager); + assertEquals(CommandConstants.INTEGER_ERROR + "\n", outContent.toString()); + restoreStreams(); + } +} diff --git a/test/core/TestSessionLog.java b/test/core/TestSessionLog.java new file mode 100644 index 0000000..91919c0 --- /dev/null +++ b/test/core/TestSessionLog.java @@ -0,0 +1,63 @@ +package core; + +import core.SessionLog; +import simulation.SimulationManager; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Rule; +import org.junit.rules.TemporaryFolder; +import org.junit.Test; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.Paths; + +public class TestSessionLog { + @Rule + public TemporaryFolder tmpdir = new TemporaryFolder(); + + @Test + public void testIsInitialized() throws IOException { + SessionLog log = new SessionLog(null); + assertFalse(log.isInitialized()); + + File tmpfile = tmpdir.newFile("testIsInitialized"); + SessionLog prevLog = new SessionLog(tmpfile.getAbsolutePath()); + assertTrue(prevLog.isInitialized()); + } + + @Test + public void testAppend() throws IOException { + File tmpfile = tmpdir.newFile("testAppend"); + SessionLog log = new SessionLog(tmpfile.getAbsolutePath()); + log.append(new String[]{"help"}); + log.append(new String[]{"load", "models.als"}); + log.append(new String[]{"step", "5"}); + assertEquals( + "help\nload models.als\nstep 5\n", + new String(Files.readAllBytes(Paths.get(tmpfile.getAbsolutePath()))) + ); + + } + + @Test + public void testRestore() throws IOException { + File tmpfile1 = tmpdir.newFile("testRestore1"); + SessionLog prevLog = new SessionLog(tmpfile1.getAbsolutePath()); + prevLog.append(new String[]{"foo", "bar"}); + prevLog.append(new String[]{"baz"}); + + File tmpfile2 = tmpdir.newFile("testRestore2"); + SessionLog log = new SessionLog(tmpfile2.getAbsolutePath()); + + SimulationManager simulationManager = new SimulationManager(); + prevLog.restore(simulationManager, log); + + assertEquals( + "foo bar\nbaz\n", + new String(Files.readAllBytes(Paths.get(tmpfile2.getAbsolutePath()))) + ); + } +} diff --git a/test/e2e/TestScenarios.java b/test/e2e/TestScenarios.java new file mode 100644 index 0000000..5153f8a --- /dev/null +++ b/test/e2e/TestScenarios.java @@ -0,0 +1,147 @@ +package e2e; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Before; +import org.junit.Rule; +import org.junit.rules.TestName; +import org.junit.Test; + +import java.io.BufferedReader; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.io.OutputStream; + +public class TestScenarios { + private StringBuilder aldbOutput; + private final String PROMPT = "(aldb) "; + + @Rule + public final TestName testName = new TestName(); + + @Before + public void init() { + aldbOutput = new StringBuilder(); + System.out.printf("Running %s...\n", testName.getMethodName()); + } + + @Test + public void testSolveRCP() throws Exception { + runALDB( + "load models/river_crossing.als", + "current", + "break \"far = Object && no near\"", + "until", + "history 10" + ); + assertOutput( + "Reading model from models/river_crossing.als...done.", + "", + "far: { }", + "near: { Chicken, Farmer, Fox, Grain }", + "\n", + "far: { Chicken, Farmer, Fox, Grain }", + "near: { }", + "\n", + "(-7)", + "----", + "far: { }", + "near: { Chicken, Farmer, Fox, Grain }", + "", + "(-6)", + "----", + "far: { Chicken, Farmer }", + "near: { Fox, Grain }", + "", + "(-5)", + "----", + "far: { Chicken }", + "near: { Farmer, Fox, Grain }", + "", + "(-4)", + "----", + "far: { Chicken, Farmer, Fox }", + "near: { Grain }", + "", + "(-3)", + "----", + "far: { Fox }", + "near: { Chicken, Farmer, Grain }", + "", + "(-2)", + "----", + "far: { Farmer, Fox, Grain }", + "near: { Chicken }", + "", + "(-1)", + "----", + "far: { Fox, Grain }", + "near: { Chicken, Farmer }", + "" + ); + } + + @Test + public void testLoadIdempotent_noEmbeddedConf() throws Exception { + runALDB( + "load models/river_crossing.als", + "load models/river_crossing.als", + "load models/river_crossing.als" + ); + assertOutput( + "Reading model from models/river_crossing.als...done.", + "Reading model from models/river_crossing.als...done.", + "Reading model from models/river_crossing.als...done." + ); + } + + @Test + public void testLoadIdempotent_embeddedConf() throws Exception { + runALDB( + "load models/musical_chairs.als", + "load models/musical_chairs.als", + "load models/musical_chairs.als" + ); + assertOutput( + "Reading model from models/musical_chairs.als...done.", + "Reading model from models/musical_chairs.als...done.", + "Reading model from models/musical_chairs.als...done." + ); + } + + @Test + public void testLoadEmbeddedConf() throws Exception { + // A model's (musical_chairs.als) embedded ParsingConf should be removed after loading a new model. + runALDB( + "load models/river_crossing.als", + "load models/musical_chairs.als", + "load models/river_crossing.als" + ); + assertOutput( + "Reading model from models/river_crossing.als...done.", + "Reading model from models/musical_chairs.als...done.", + "Reading model from models/river_crossing.als...done." + ); + } + + private void runALDB(String... inputLines) throws Exception { + Process aldb = Runtime.getRuntime().exec("java -jar dist/aldb.jar"); + OutputStream aldbIn = aldb.getOutputStream(); + String input = String.join("\n", inputLines) + "\n"; + aldbIn.write(input.getBytes()); + aldbIn.close(); + + BufferedReader aldbOut = new BufferedReader(new InputStreamReader(aldb.getInputStream())); + String line; + while ((line = aldbOut.readLine()) != null) { + aldbOutput.append(line + "\n"); + } + aldbOutput.deleteCharAt(aldbOutput.length() - 1); + + aldb.waitFor(); + } + + private void assertOutput(String... outputLines) { + assertEquals(String.join("\n", outputLines) + "\n", aldbOutput.toString().replace(PROMPT, "")); + } +} diff --git a/test/simulation/TestConstraintManager.java b/test/simulation/TestConstraintManager.java new file mode 100644 index 0000000..880a672 --- /dev/null +++ b/test/simulation/TestConstraintManager.java @@ -0,0 +1,60 @@ +package simulation; + +import simulation.ConstraintManager; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +import java.util.ArrayList; +import java.util.List; + +public class TestConstraintManager { + @Test + public void testAddConstraint() { + ConstraintManager cm = new ConstraintManager(); + String c1 = "a=b"; + String c2 = "c=d"; + cm.addConstraint(c1); + cm.addConstraint(c2); + List expected = new ArrayList(); + expected.add(c1); + expected.add(c2); + assertEquals(expected, cm.getConstraints()); + } + + @Test + public void testRemoveConstraint() { + ConstraintManager cm = new ConstraintManager(); + String c1 = "a=b"; + String c2 = "c=d"; + cm.addConstraint(c1); + cm.addConstraint(c2); + assertTrue(cm.removeConstraint(1)); + assertTrue(cm.removeConstraint(2)); + assertFalse(cm.removeConstraint(3)); + assertEquals(new ArrayList(), cm.getConstraints()); + } + + @Test + public void testClearConstraints() { + ConstraintManager cm = new ConstraintManager(); + String c1 = "a=b"; + String c2 = "c=d"; + cm.addConstraint(c1); + cm.addConstraint(c2); + cm.clearConstraints(); + assertEquals(new ArrayList(), cm.getConstraints()); + } + + @Test + public void testGetFormattedConstraints() { + ConstraintManager cm = new ConstraintManager(); + String c1 = "a=b"; + String c2 = "c=d"; + cm.addConstraint(c1); + cm.addConstraint(c2); + String expected = "\nNum Constraint\n1 a=b\n2 c=d\n"; + assertEquals(expected, cm.getFormattedConstraints()); + } +} diff --git a/test/simulation/TestSimulationManager.java b/test/simulation/TestSimulationManager.java new file mode 100644 index 0000000..be77dd1 --- /dev/null +++ b/test/simulation/TestSimulationManager.java @@ -0,0 +1,431 @@ +package simulation; + +import alloy.AlloyInterface; +import alloy.ParsingConf; + +import edu.mit.csail.sdg.translator.A4Solution; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Before; +import org.junit.Rule; +import org.junit.rules.TemporaryFolder; +import org.junit.Test; + +import java.io.File; +import java.io.IOException; +import java.nio.file.Files; +import java.nio.file.StandardCopyOption; +import java.nio.file.StandardOpenOption; +import java.util.ArrayList; +import java.util.HashMap; +import java.util.List; +import java.util.Map; + +public class TestSimulationManager { + private SimulationManager sm; + private File modelFile; + + @Rule + public TemporaryFolder tempFolder = new TemporaryFolder(); + + @Before + public void init() { + sm = new SimulationManager(); + } + + @Test + public void testInitializeWithModel() throws IOException { + initializeTestWithModelPath("models/switch.als"); + String expectedDOTString = String.join("\n", + "digraph graphname {", + "\tS1", + "}", + "" + ); + assertTrue(sm.initializeWithModel(modelFile)); + assertTrue(sm.isInitialized()); + assertFalse(sm.isTrace()); + assertEquals(expectedDOTString, sm.getDOTString()); + } + + @Test + public void testInitializeWithModel_nonexistantFile() { + File nonexistantFile = new File("nonexistant-file"); + assertFalse(sm.initializeWithModel(nonexistantFile)); + assertFalse(sm.isInitialized()); + } + + @Test + public void testInitializeWithModel_noInitPredicate() throws IOException { + String noInitModel = String.join("\n", + "sig State {}", + "pred next[s, s': State] {}", + "" + ); + initializeTestWithModelString(noInitModel); + assertFalse(sm.initializeWithModel(modelFile)); + assertFalse(sm.isInitialized()); + } + + @Test + public void testInitializeWithModel_noNextPredicate() throws IOException { + String noNextModel = String.join("\n", + "sig State {}", + "pred init[s: State] {}", + "" + ); + initializeTestWithModelString(noNextModel); + assertFalse(sm.initializeWithModel(modelFile)); + assertFalse(sm.isInitialized()); + } + + @Test + public void testInitializeWithModel_syntaxError_incompletePredicate() throws IOException { + String invalidModel = String.join("\n", + "sig State {}", + "pred init[s: State] {", + "" + ); + initializeTestWithModelString(invalidModel); + assertFalse(sm.initializeWithModel(modelFile)); + assertFalse(sm.isInitialized()); + } + + @Test + public void testInitializeWithTrace() throws IOException { + File traceFile = createTrace(); + + assertTrue(sm.initializeWithTrace(traceFile)); + assertTrue(sm.isTrace()); + } + + @Test + public void testInitializeWithTrace_invalidXML() throws IOException { + initializeTestWithModelPath("models/switch.als"); + assertFalse(sm.initializeWithTrace(modelFile)); + assertFalse(sm.isTrace()); + } + + @Test + public void testPerformStep_model() throws IOException { + initializeTestWithModelPath("models/switch.als"); + String expectedDOTString = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2 -> S1", + "}", + "" + ); + String expectedCurrentState = String.join("\n", + "", + "a: { On }", + "b: { Off }", + "" + ); + String expectedHistory = String.join("\n", + "", + "(-2)", + "----", + "a: { On }", + "b: { Off }", + "", + "(-1)", + "----", + "a: { Off }", + "b: { On }", + "" + ); + sm.initializeWithModel(modelFile); + sm.performStep(2); + assertEquals(expectedDOTString, sm.getDOTString()); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + assertEquals(expectedHistory, sm.getHistory(2)); + } + + @Test + public void testPerformStep_modelWithScopes() throws IOException { + String content = String.join("\n", + "transitionRelationName: trans", + "additionalSigScopes:", + " Chair: 3", + " Player: 4" + ); + ParsingConf pc = ParsingConf.initializeWithYaml(content); + + initializeTestWithModelPath("models/musical_chairs.als"); + String expectedDOTString = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2 -> S3", + "\tS3", + "}", + "" + ); + String expectedCurrentState = String.join("\n", + "", + "mode: { sitting }", + "players: { Player_0, Player_1, Player_2, Player_3 }", + "chairs: { Chair_0, Chair_1, Chair_2 }", + "occupied: { Chair_0->Player_2, Chair_1->Player_1, Chair_2->Player_0 }", + "" + ); + String expectedHistory = String.join("\n", + "", + "(-2)", + "----", + "mode: { start }", + "players: { Player_0, Player_1, Player_2, Player_3 }", + "chairs: { Chair_0, Chair_1, Chair_2 }", + "occupied: { }", + "", + "(-1)", + "----", + "mode: { walking }", + "players: { Player_0, Player_1, Player_2, Player_3 }", + "chairs: { Chair_0, Chair_1, Chair_2 }", + "occupied: { }", + "" + ); + + sm.setParsingConf(pc); + assertTrue(sm.initializeWithModel(modelFile)); + sm.performStep(2); + assertEquals(expectedDOTString, sm.getDOTString()); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + assertEquals(expectedHistory, sm.getHistory(2)); + } + + @Test + public void testPerformStep_trace() throws IOException { + File traceFile = createTrace(); + String expectedDOTString = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2", + "}", + "" + ); + String expectedCurrentState = String.join("\n", + "", + "a: { On }", + "b: { Off }", + "" + ); + String expectedHistory = String.join("\n", + "", + "(-1)", + "----", + "a: { Off }", + "b: { On }", + "" + ); + + assertTrue(sm.initializeWithTrace(traceFile)); + assertTrue(sm.isTrace()); + sm.performStep(1); + assertEquals(expectedDOTString, sm.getDOTString()); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + assertEquals(expectedHistory, sm.getHistory(1)); + } + + @Test + public void testPerformReverseStep_model() throws IOException { + initializeTestWithModelPath("models/switch.als"); + String expectedDOTString = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2 -> S1", + "}", + "" + ); + String expectedCurrentState = String.join("\n", + "", + "a: { On }", + "b: { Off }", + "" + ); + String expectedHistory = String.join("\n", + "", + "(-2)", + "----", + "a: { On }", + "b: { Off }", + "", + "(-1)", + "----", + "a: { Off }", + "b: { On }", + "" + ); + sm.initializeWithModel(modelFile); + sm.performStep(4); + sm.performReverseStep(2); + assertEquals(expectedDOTString, sm.getDOTString()); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + assertEquals(expectedHistory, sm.getHistory(2)); + } + + @Test + public void testPerformReverseStep_trace() throws IOException { + File traceFile = createTrace(); + String expectedDOTString = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2", + "}", + "" + ); + String expectedCurrentState = String.join("\n", + "", + "a: { Off }", + "b: { On }", + "" + ); + + assertTrue(sm.initializeWithTrace(traceFile)); + assertTrue(sm.isTrace()); + sm.performStep(1); + sm.performReverseStep(1); + assertEquals(expectedDOTString, sm.getDOTString()); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + } + + @Test + public void testSelectAlternatePath() throws IOException { + initializeTestWithModelPath("models/river_crossing.als"); + String expectedCurrentState = String.join("\n", + "", + "far: { }", + "near: { Farmer, Fox, Grain }", + "" + ); + String expectedAlternateState = String.join("\n", + "", + "far: { Grain }", + "near: { Farmer, Fox }", + "" + ); + + sm.initializeWithModel(modelFile); + sm.performStep(2); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + String history = sm.getHistory(2); + assertTrue(sm.selectAlternatePath(false)); + assertEquals(expectedAlternateState, sm.getCurrentStateString()); + // History should still be unchanged. + assertEquals(history, sm.getHistory(2)); + } + + @Test + public void testSelectAlternatePath_reverse() throws IOException { + initializeTestWithModelPath("models/river_crossing.als"); + String expectedCurrentState = String.join("\n", + "", + "far: { }", + "near: { Farmer, Fox, Grain }", + "" + ); + String expectedAlternateState = String.join("\n", + "", + "far: { Grain }", + "near: { Farmer, Fox }", + "" + ); + + sm.initializeWithModel(modelFile); + sm.performStep(2); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + String history = sm.getHistory(2); + assertTrue(sm.selectAlternatePath(false)); + assertTrue(sm.selectAlternatePath(false)); + assertTrue(sm.selectAlternatePath(true)); + assertEquals(expectedAlternateState, sm.getCurrentStateString()); + // History should still be unchanged. + assertEquals(history, sm.getHistory(2)); + } + + @Test + public void testSelectAlternatePath_noActiveSolutions() throws IOException { + initializeTestWithModelPath("models/switch.als"); + sm.initializeWithModel(modelFile); + assertFalse(sm.selectAlternatePath(false)); + } + + @Test + public void testSelectAlternatePath_noValidAlternates() throws IOException { + initializeTestWithModelPath("models/switch.als"); + sm.initializeWithModel(modelFile); + sm.performStep(2); + assertFalse(sm.selectAlternatePath(false)); + } + + @Test + public void testSelectAlternatePath_reverse_noValidAlternates() throws IOException { + initializeTestWithModelPath("models/switch.als"); + sm.initializeWithModel(modelFile); + sm.performStep(2); + sm.performReverseStep(1); + assertFalse(sm.selectAlternatePath(true)); + } + + @Test + public void testPerformUntil() throws IOException { + initializeTestWithModelPath("models/switch.als"); + sm.initializeWithModel(modelFile); + ConstraintManager cm = sm.getConstraintManager(); + String constraint = "a = Off"; + cm.addConstraint(constraint); + String expectedCurrentState = String.join("\n", + "", + "a: { Off }", + "b: { On }", + "" + ); + + assertTrue(sm.performUntil(10)); + assertEquals(expectedCurrentState, sm.getCurrentStateString()); + } + + @Test + public void testValidateConstraint() throws IOException { + initializeTestWithModelPath("models/switch.als"); + sm.initializeWithModel(modelFile); + String constraint = "a = Off"; + assertTrue(sm.validateConstraint(constraint)); + } + + @Test + public void testValidateConstraint_invalid() throws IOException { + initializeTestWithModelPath("models/switch.als"); + sm.initializeWithModel(modelFile); + String constraint = "ab = Off"; + assertFalse(sm.validateConstraint(constraint)); + } + + private void initializeTestWithModelPath(String modelPath) throws IOException { + File file = new File(modelPath); + modelFile = tempFolder.newFile("test.als"); + Files.copy(file.toPath(), modelFile.toPath(), StandardCopyOption.REPLACE_EXISTING); + } + + private void initializeTestWithModelString(String modelString) throws IOException { + modelFile = tempFolder.newFile("test.als"); + Files.write(modelFile.toPath(), modelString.getBytes()); + } + + private File createTrace() throws IOException { + initializeTestWithModelPath("models/switch.als"); + String alloyModelString = new String(Files.readAllBytes(modelFile.toPath())); + + String commandString = "\nrun {} for 4 State"; + Files.write(modelFile.toPath(), commandString.getBytes(), StandardOpenOption.APPEND); + + A4Solution sol = AlloyInterface.run(AlloyInterface.compile(modelFile.getPath())); + File traceFile = tempFolder.newFile("test.xml"); + Map sources = new HashMap(); + sources.put(modelFile.getPath(), alloyModelString); + sol.writeXML(traceFile.getPath(), null, sources); + return traceFile; + } +} diff --git a/test/state/TestStateGraph.java b/test/state/TestStateGraph.java new file mode 100644 index 0000000..3e20d7a --- /dev/null +++ b/test/state/TestStateGraph.java @@ -0,0 +1,128 @@ +package state; + +import edu.mit.csail.sdg.ast.Sig.*; + +import alloy.SigData; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +import java.util.ArrayList; +import java.util.List; + +public class TestStateGraph { + private StateGraph stateGraph = new StateGraph(); + + @Test + public void testInitWithNodes() { + List nodes = createNewStateNodeList(3); + String expected = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2 -> S3", + "\tS3", + "}", + "" + ); + stateGraph.initWithNodes(nodes); + assertEquals(expected, stateGraph.getDOTString()); + assertEquals(3, stateGraph.size()); + } + + @Test + public void testInitWithNodes_empty() { + List nodes = new ArrayList<>();; + String expected = String.join("\n", + "digraph graphname {", + "}", + "" + ); + stateGraph.initWithNodes(nodes); + assertEquals(expected, stateGraph.getDOTString()); + assertEquals(0, stateGraph.size()); + } + + @Test + public void testAddNodes_cycle() { + List initialNodes = createNewStateNodeList(2); + StateNode startNode = initialNodes.get(1); + startNode.addValueToField("g", "diff_val"); + stateGraph.initWithNodes(initialNodes); + List newNodes = createNewStateNodeList(1); + String expected = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2 -> S1", + "}", + "" + ); + stateGraph.addNodes(startNode, newNodes); + assertEquals(expected, stateGraph.getDOTString()); + assertEquals(2, stateGraph.size()); + } + + @Test + public void testAddNodes_existingNodes() { + List initialNodes = createNewStateNodeList(2); + stateGraph.initWithNodes(initialNodes); + List newExistingNodes = createNewStateNodeList(4); + StateNode startNode = initialNodes.get(0); + String expected = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS2", + "}", + "" + ); + stateGraph.addNodes(startNode, newExistingNodes); + assertEquals(expected, stateGraph.getDOTString()); + assertEquals(2, stateGraph.size()); + } + + @Test + public void testAddNodes_newNodes() { + List initialNodes = createNewStateNodeList(2); + stateGraph.initWithNodes(initialNodes); + List newNodes = new ArrayList<>(); + SigData sigData = new SigData(createNewSig()); + StateNode a = new StateNode(sigData, null); + StateNode b = new StateNode(sigData, null); + // Ensure that nodes a and b are not equal. + a.addValueToField("g", "val1"); + b.addValueToField("g", "val2"); + newNodes.add(a); + newNodes.add(b); + StateNode startNode = initialNodes.get(0); + String expected = String.join("\n", + "digraph graphname {", + "\tS1 -> S2", + "\tS1 -> S3", + "\tS2", + "\tS3 -> S4", + "\tS4", + "}", + "" + ); + stateGraph.addNodes(startNode, newNodes); + assertEquals(expected, stateGraph.getDOTString()); + assertEquals(4, stateGraph.size()); + } + + // Create a list with `amount` nodes that are all equal. + private List createNewStateNodeList(int amount) { + List nodes = new ArrayList<>(); + SigData sigData = new SigData(createNewSig()); + for (int i = 0; i < amount; i++) { + nodes.add(new StateNode(sigData, null)); + } + return nodes; + } + + private PrimSig createNewSig() { + PrimSig sigA = new PrimSig("A"); + PrimSig sigB = new PrimSig("B"); + Field f2 = sigA.addField("g", sigB); + return sigA; + } +} diff --git a/test/state/TestStateNode.java b/test/state/TestStateNode.java new file mode 100644 index 0000000..7df1bb2 --- /dev/null +++ b/test/state/TestStateNode.java @@ -0,0 +1,189 @@ +package state; + +import edu.mit.csail.sdg.ast.Sig; + +import alloy.SigData; +import alloy.ParsingConf; +import state.StateNode; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Before; +import org.junit.Test; + +public class TestStateNode { + private StateNode stateNode; + + @Before + public void init() { + SigData sigData = new SigData(createNewSig()); + stateNode = new StateNode(sigData, new ParsingConf()); + } + + @Test + public void testAddStep() { + SigData sigData = new SigData(createNewSig()); + StateNode stateNode2 = new StateNode(sigData, new ParsingConf()); + stateNode2.setIdentifier(2); + stateNode.setIdentifier(1); + stateNode.addStep(stateNode2); + assertEquals(2, stateNode.getSteps().get(0).getIdentifier()); + } + + @Test + public void testToString() { + String expected = String.join("\n", + "", + "f: { string1, string2 }", + "g: { string }", + "" + ); + stateNode.addValueToField("f", "string1"); + stateNode.addValueToField("f", "string2"); + stateNode.addValueToField("g", "string"); + assertEquals(expected, stateNode.toString()); + } + + @Test + public void testAddValueToField_sortOrder() { + String expected = String.join("\n", + "", + "f: { A, B, R, a, b }", + "g: { 1, 2, 3, 4, 5 }", + "" + ); + stateNode.addValueToField("f", "B"); + stateNode.addValueToField("f", "a"); + stateNode.addValueToField("f", "A"); + stateNode.addValueToField("f", "R"); + stateNode.addValueToField("f", "b"); + stateNode.addValueToField("g", "5"); + stateNode.addValueToField("g", "4"); + stateNode.addValueToField("g", "3"); + stateNode.addValueToField("g", "1"); + stateNode.addValueToField("g", "2"); + assertEquals(expected, stateNode.toString()); + } + + @Test + public void testStringForProperty() { + String expected = String.join("\n", + "", + "string1", + "string2", + "string3", + "" + ); + stateNode.addValueToField("f", "string1"); + stateNode.addValueToField("f", "string2"); + stateNode.addValueToField("f", "string3"); + assertEquals(expected, stateNode.stringForProperty("f")); + } + + @Test + public void testStringForProperty_notFound() { + String expected = "Property not found."; + stateNode.addValueToField("f", "string1"); + assertEquals(expected, stateNode.stringForProperty("x")); + } + + @Test + public void testGetDiffString() { + SigData sigData = new SigData(createNewSig()); + StateNode stateNode2 = new StateNode(sigData, new ParsingConf()); + String expected = String.join("\n", + "", + "f: { string1, string2 }", + "" + ); + stateNode.addValueToField("f", "string1"); + stateNode.addValueToField("f", "string2"); + assertEquals(expected, stateNode.getDiffString(stateNode2)); + } + + @Test + public void testGetDiffString_null() { + String expected = String.join("\n", + "", + "f: { string1, string2 }", + "g: { string }", + "" + ); + stateNode.addValueToField("f", "string1"); + stateNode.addValueToField("f", "string2"); + stateNode.addValueToField("g", "string"); + assertEquals(expected, stateNode.getDiffString(null)); + } + + @Test + public void testEquals() { + SigData sigData = new SigData(createNewSig()); + StateNode stateNode2 = new StateNode(sigData, new ParsingConf()); + StateNode stateNode3 = new StateNode(sigData, new ParsingConf()); + // reflexive: + assertTrue(stateNode.equals(stateNode)); + // symmetric: + assertTrue(stateNode.equals(stateNode2)); + assertTrue(stateNode2.equals(stateNode)); + // transitive: + assertTrue(stateNode.equals(stateNode2)); + assertTrue(stateNode2.equals(stateNode3)); + assertTrue(stateNode.equals(stateNode3)); + // consistent: + assertTrue(stateNode.equals(stateNode2)); + assertTrue(stateNode.equals(stateNode2)); + assertTrue(stateNode.equals(stateNode2)); + // null values: + assertFalse(stateNode.equals(null)); + } + + @Test + public void testNotEquals_differentFieldValues() { + SigData sigData = new SigData(createNewSig()); + StateNode stateNode2 = new StateNode(sigData, new ParsingConf()); + stateNode.addValueToField("f", "string1"); + assertFalse(stateNode.equals(stateNode2)); + assertFalse(stateNode2.equals(stateNode)); + } + + @Test + public void testNotEquals_differentFields() { + Sig sigA = createNewSig(); + Sig sigC = new Sig.PrimSig("C"); + Sig.Field f = sigA.addField("h", sigC); + SigData sigData = new SigData(sigA); + StateNode stateNode2 = new StateNode(sigData, new ParsingConf()); + assertFalse(stateNode.equals(stateNode2)); + assertFalse(stateNode2.equals(stateNode)); + } + + @Test + public void testGetAlloyInitString() { + String expected = String.join("\n", + "", + "pred init[s: State] {", + "\ts.f = string1 + string2", + "\ts.g = string", + "}", + "" + ); + stateNode.addValueToField("f", "string1"); + stateNode.addValueToField("f", "string2"); + stateNode.addValueToField("g", "string"); + assertEquals(expected, stateNode.getAlloyInitString()); + } + + @Test + public void testIdentifier() { + stateNode.setIdentifier(5); + assertEquals(5, stateNode.getIdentifier()); + } + + private Sig createNewSig() { + Sig sigA = new Sig.PrimSig("A"); + Sig sigB = new Sig.PrimSig("B"); + Sig.Field f1 = sigA.addField("f", sigB.lone_arrow_lone(sigB)); + Sig.Field f2 = sigA.addField("g", sigB); + return sigA; + } +} diff --git a/test/state/TestStatePath.java b/test/state/TestStatePath.java new file mode 100644 index 0000000..675832d --- /dev/null +++ b/test/state/TestStatePath.java @@ -0,0 +1,233 @@ +package state; + +import edu.mit.csail.sdg.ast.Sig.PrimSig; + +import alloy.SigData; +import state.StateNode; +import state.StatePath; + +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.Test; + +import java.util.ArrayList; +import java.util.List; + +public class TestStatePath { + StateNode n0 = new StateNode(new SigData(new PrimSig("a")), null); + StateNode n1 = new StateNode(new SigData(new PrimSig("b")), null); + StateNode n2 = new StateNode(new SigData(new PrimSig("c")), null); + + @Test + public void testInitWithPath() { + StatePath sp = new StatePath(); + List path = new ArrayList(); + path.add(n0); + path.add(n1); + sp.initWithPath(path); + + assertFalse(sp.isEmpty()); + assertEquals(n0, sp.getNode(0)); + assertEquals(n1, sp.getNode(1)); + assertEquals(1, sp.getPosition()); + + // Should be idempotent with the same input path. + sp.initWithPath(path); + assertFalse(sp.isEmpty()); + assertEquals(n0, sp.getNode(0)); + assertEquals(n1, sp.getNode(1)); + assertEquals(1, sp.getPosition()); + } + + @Test + public void testIsEmpty() { + StatePath sp = new StatePath(); + assertTrue(sp.isEmpty()); + + List path = new ArrayList(); + path.add(n0); + sp.initWithPath(path); + assertFalse(sp.isEmpty()); + } + + @Test + public void testGetNode() { + StatePath sp = new StatePath(); + assertEquals(null, sp.getNode(-1)); + assertEquals(null, sp.getNode(0)); + + List path = new ArrayList(); + path.add(n0); + sp.initWithPath(path); + assertEquals(n0, sp.getNode(0)); + assertEquals(null, sp.getNode(1)); + } + + @Test + public void testGetCurNode() { + StatePath sp = new StatePath(); + assertEquals(null, sp.getCurNode()); + + List path = new ArrayList(); + path.add(n0); + path.add(n1); + sp.initWithPath(path); + + assertEquals(n1, sp.getCurNode()); + } + + @Test + public void testGetPrevNode() { + StatePath sp = new StatePath(); + assertEquals(null, sp.getPrevNode()); + + List path = new ArrayList(); + path.add(n0); + path.add(n1); + sp.initWithPath(path); + assertEquals(null, sp.getPrevNode()); + + sp.setPosition(0); + assertEquals(n1, sp.getPrevNode()); + } + + @Test + public void testSetAndGetPosition() { + StatePath sp = new StatePath(); + assertEquals(0, sp.getPosition()); + + List path = new ArrayList(); + path.add(n0); + path.add(n1); + sp.initWithPath(path); + assertEquals(1, sp.getPosition()); + + sp.setPosition(0); + assertEquals(n1, sp.getPrevNode()); + assertEquals(0, sp.getPosition()); + } + + @Test + public void testIncrementPosition() { + StatePath sp = new StatePath(); + List path = new ArrayList(); + path.add(n0); + path.add(n1); + sp.initWithPath(path); + sp.setPosition(0); + assertEquals(0, sp.getPosition()); + + sp.incrementPosition(1); + assertEquals(1, sp.getPosition()); + assertEquals(n0, sp.getPrevNode()); + } + + @Test + public void testDecrementPosition() { + // Decrement path size 3 by 1. + StatePath sp = new StatePath(); + List path = new ArrayList(); + path.add(n0); + path.add(n1); + path.add(n2); + sp.initWithPath(path); + + sp.decrementPosition(1, false); + assertEquals(1, sp.getPosition()); + assertEquals(n0, sp.getPrevNode()); + assertEquals(n1, sp.getCurNode()); + + // Decrement path size 3 by 2. + sp = new StatePath(); + sp.initWithPath(path); + + sp.decrementPosition(2, false); + assertEquals(0, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(n0, sp.getCurNode()); + + // Decrement path size 3 by 3. + sp = new StatePath(); + sp.initWithPath(path); + + sp.decrementPosition(3, false); + assertEquals(0, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(n0, sp.getCurNode()); + + // Decrement path size 3 by 4. + sp = new StatePath(); + sp.initWithPath(path); + + sp.decrementPosition(4, false); + assertEquals(0, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(n0, sp.getCurNode()); + } + + @Test + public void testSetTempPath() { + StatePath sp = new StatePath(); + List tempPath = new ArrayList(); + tempPath.add(n0); + tempPath.add(n1); + sp.setTempPath(tempPath); + assertEquals(1, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(n1, sp.getCurNode()); + } + + @Test + public void testClearTempPath() { + // Clear temp path with no initial path set. + StatePath sp = new StatePath(); + List tempPath = new ArrayList(); + tempPath.add(n0); + tempPath.add(n1); + sp.setTempPath(tempPath); + + sp.clearTempPath(); + assertEquals(-1, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(null, sp.getCurNode()); + + // Clear temp path with an initial path set. + sp.initWithPath(tempPath); + + // Should be a no-op. + sp.clearTempPath(); + assertEquals(1, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(n1, sp.getCurNode()); + + sp.setTempPath(tempPath); + sp.clearTempPath(); + assertEquals(1, sp.getPosition()); + assertEquals(null, sp.getPrevNode()); + assertEquals(n1, sp.getCurNode()); + } + + @Test + public void testGetHistory() { + StatePath sp = new StatePath(); + assertEquals("", sp.getHistory(0, false)); + assertEquals("", sp.getHistory(0, true)); + assertEquals("", sp.getHistory(1, false)); + assertEquals("", sp.getHistory(1, true)); + + List path = new ArrayList(); + path.add(n0); + path.add(n1); + path.add(n2); + sp.initWithPath(path); + + assertEquals("\n(-2)\n----\n\n(-1)\n----\n", sp.getHistory(3, false)); + assertEquals("\n(-2)\n----\n\n(-1)\n----\n", sp.getHistory(3, true)); + assertEquals("\n(-2)\n----\n\n(-1)\n----\n", sp.getHistory(2, false)); + assertEquals("\n(-2)\n----\n\n(-1)\n----\n", sp.getHistory(2, true)); + assertEquals("\n(-1)\n----\n", sp.getHistory(1, false)); + assertEquals("\n(-1)\n----\n", sp.getHistory(1, true)); + assertEquals("", sp.getHistory(0, false)); + assertEquals("", sp.getHistory(0, true)); + } +} diff --git a/traces/fgs_conf.yml b/traces/fgs_conf.yml new file mode 100644 index 0000000..7ee86c3 --- /dev/null +++ b/traces/fgs_conf.yml @@ -0,0 +1,2 @@ +# Name of the sig representing the main state in the Alloy model. +stateSigName: Snapshot diff --git a/traces/fgs_counterexample.xml b/traces/fgs_counterexample.xml new file mode 100644 index 0000000..c67b5f2 --- /dev/null +++ b/traces/fgs_counterexample.xml @@ -0,0 +1,1564 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +