Add parser and model builder for JANI format

[keb77]

No description provided.

[EnricoGhiorzi]

Thank you for your PR! I will review it in detail, but, for a start, could you make sure the code is formatted using cargo fmt? As you see, there is an automated check that fails because of that.

[keb77]

@EnricoGhiorzi I formatted the code and pushed the changes. Thank you!

[EnricoGhiorzi]

The code looks good but I would like to have some automated tests. I will add a test.rs file that does that but the two examples we can run do not terminate. Why do you think that is the case?

[EnricoGhiorzi]

I managed to run this test: parse the jani file, build the channel system, and run random actions on it. I would expect the channel system to terminate (meaning to get to a state in which no more transitions are possible), instead it seems to run forever. Do you have any idea why? Same applies for test.jani.

[keb77]

I believe the problem is caused by the issue we discussed during our last meeting regarding how global variables are handled: in a program graph where a transition has a guard containing global variables, the system continuously checks for updates to those variables (which is done through other transitions). This should be why test.jani doesn't terminate. test2.jani, on the other hand, is structured in a way that should terminate, but it probably gets caught in a loop for similar reasons because the test function always chooses the first element in the possible transitions list. I modified the test function to select random transitions instead and it terminates as expected.

[EnricoGhiorzi]

Your last commit has no sign-off and it fails the automated test. Could you fix that?

Also, would it be possible to modify test.jani so that it eventually terminates too? That would make a good automated test.

[keb77]

All done!

[EnricoGhiorzi]

The code looks good to me!