Time simulations

[anaisac]

I've understood that the simulation of realizable requirements is only available using the jkind engine, but I would like to understand why is not possible with the other engines (kind2 and MBP variants).
Is this something that will be supported in the future?
I'm still trying to figure out a use case for the MBP variants or why they are able to complement the jkind/kind2 engines,

[andreaskatis]

Hi @anaisac ,

Regarding the MBP variants, see my response in your other post here: #116

Currently, Kind 2 does not have an option to provide example execution traces for realizable requirements, in the way that JKind does. I will ask the Kind 2 developers to see if they would be interested in providing such an option in the future.

In the meantime, if you have specific feedback regarding the option using JKind please let me know.

Best,

Andreas

[anaisac]

Hi @andreaskatis

Regarding MBP i'm clarified :)

I think it could be interesting to compare the execution traces for realizable requirements between the engines. If they would be interested in providing that in the future I would like to keep up with those features.

Currently, I'm going to try to solve my issue of discrepancy between both engines and then, maybe I can have more feedback. I will keep you in the loop.

Thank you,
Anaísa