kk578 / umlaut Goto Github PK

Agree with uml-annotator on layout, then parse string into objects for smt-generator.

Automate all steps into a script call.

User annotates UML -> AnnotatedUML

1. UML-Parser parses AnnotatedUML into ParsedAnnotatedUML
2. SMT-Generator reads ParsedAnnotatedUML and creates SMTScript
3. SMT-Generator runs SMTScript and creates ModelTestInputs
4. Test-Generator reads ParsedAnnotatedUML and ModelTestInputs and creates TestSuite

Give each pre/post-condition a unique ID.

Assists in solving #2.

smt-solver spawns z3 to run.

Install onto Travis and keep cached?

Can use a CFG to more reliably handle pulling data from the model through uml-parser.

Similar to #61.

Currently only updates the file that is being used.
Ideal would be to select .uml file to load and that can push updates to the .classdiagram files.

This is a major issue if you want to work on the model again after doing the annotations.
It is slightly difficult to implement due to GUIDs need to match between the files, under <elementDefinition> nodes.

Merge all package.json together to a top level item.
Move subprojects down into a src/ directory.

No need for postinstall script if this is done.

Loses some sense of how the codebase is moduled however.

Z3 requires = to do equality, whereas programming languages can differ but mostly use ==.

Read existing conditions into OclCondition object format.

Minor cleanup to group together the smt-solver.

For the first prototype, keep split outside Visual Studio to workaround having to work with Modeling SDK.

If it speeds up the time taken and is worth the speed, may be useful.

Number of conditions may not be large enough for this to matter however.

More representative in the future for conditions that may not be solvable just by SMT.
(Generator part of name works, but may be confusing with refactor of test-generator to top level.)

E.g. Input-Generator, Input-Solver, Test-Inputs

Would like to update to BSD-3-Clause.

Need confirming whether this can be made public and open source.

Copy Nunit generator and just modify the template to determine if anything needs to change particularly

Keep this in a config for expanding and so that can reuse in later steps (test-generator).

Rework the splitting of results and handle strings directly within the parser.

Save some time on Travis.
Can run codecov using ./node_modules/.bin/codecov.

Could pass SMT-LIB2 strings directly to z3 to avoid requiring to store state to a file.

Currently assuming no methods have multiple overloads.
Is this a worthwhile thing to handle?

Test utility objects.

SMT-Solver should create the folders that the SMT files will be stored in temporarily for passing to Z3.

• Floats
• Doubles

Refactor this after #21.

Using some hacky string manipulation at the current time, where a CFG would be much better suited.

smt-solver does not correctly build items for multiple classes at once.

Do no prior string manipulation on the conditions, and allow CFG to parse entirely.
Can then remove ----- splitters and leave as empty or just spaces.

Unit tests:

• Annotator
• UML-Parser
• Input-Generator
• Test-Generator

Analyse class for all class variables and arguments to the method.

SMT-generator has additional items that should be removed.

Strength of typing introduces challenges to the parser and test generation.
Assuming only Strongly typed for now.

Evaluate how to handle weakly typed languages later. (Add it to the test suite?)

Write conditions into standardised form into method's pre/post-condition property (Visual Studio) listing.

Check CodeCov for free private repo.

Support the generation of tests for multiple classes at once.

Annotator should have another button to delete the currently selected condition

Currently is hardcoded against building for the SimpleMath test project.

Add linting and tests

Need C# linter and code runner on terminal though.

Add a utilities to handle comparisons and conversions.

Keep all code used for testing project together and up to date

• SimpleMath
• IntegerStack

Add an expected exception state to conditions.

UML-Parser needs to split this into a exception property under the condition.
SMT-Generator and Test-Generator already handles this.

Include details of the entire universe of inputs for each test rather than just the one that is invalid.

Parse VS Class diagram file as a XML configuration, into the annotator program.

Require by class, all methods and variables and expose the invariants/preconditions/postconditions.

Z3 requires (not (= a a)), where it is currently being stored as != in the parsed uml.

Populating the list dynamically opens up support for plugins to other forms of UML objects.

Search locally installed npm modules with some plugin name/keyword (TBD).

Add exceptions that should be thrown if a given condition is unsatisfied.

Object describing the exception should be added to the UML Object.

Nodes are generated in annotator without IDs, which seem to get ignored by Visual Studio.

Parser expects a list of variables and list of methods to exist in order for it to successfully do anything.