Brandhoej commented 2 years ago

Fixes quotient and removes redundant Location classes (SymbolicLocation, ComplexLocation, SimpleLocation, UniversalLocation, InconsistentLocation).

Description

selfLoopNonZeno.xml file was used in a test and caused the CI to fail as the file was placed in the incorrect directory. It is now in samples/xml which fixes this issue.
GrpcServer Used port 80 which caused port conflicts when running without a port specification, as this is the standard HTTP port. Changing it to port 9000 fixes this.
Print statements have been replaced to use Log.
``instanceof```for locations (Mostly Symbolic Location in e.g. Quotient) have been replaced with matching property getters.
Quotient now uses a common way of generating the Automaton, which then allowed us to remove some tests taking too long with Quotient Automaton generation such as newQuotientTest4AAutomaton.
e2e tests now supports xml file configurations.
The location now have factory methods instead of public construtors which allows us to handle memory with object pools later.

Opens

If this PR gets merged then I think the following issues should be opened:

Opened #84: GrpcServer now uses port 9000 but we should consider to dynamically find an available port instead of hardcoding it.
Opened #86: As Quotient now uses a common interface for generating its Automaton, we have to move Bisimilarity preparation into the TransitionSystem and Automaton class.
The e2e consistency tests are ignored because they cause a internal CDD error when running them in the CI.
Relating to #62 I found that we use two different invariants for Inconsistent locations, the zero and true cdd (Both the true guard). The factory method for inconsistent locations should take the x_new clock created. However, correcting the invariant caused some tests to fail.

closes #71 closes #72 closes #65

magoorden commented 2 years ago

Th CI pipeline is finally running the tests. One test case is failing. @Brandhoej is this the test case we talked about last Monday?

Brandhoej commented 2 years ago

Th CI pipeline is finally running the tests. One test case is failing. @Brandhoej is this the test case we talked about last Monday?

@magoorden I found that the CI was not running because of a merge conflict, and yes it is the "Various" "testFromFramework4".

magoorden commented 2 years ago

Remember to open issues for those mentioned in the merge request description.