Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Simulate option is unavailable even when realizability analysis with JKind Passes #102

Closed
smithdtyler opened this issue Dec 13, 2024 · 3 comments

Comments

@smithdtyler
Copy link

I analyzed the requirements for my Microwave project with JKind, but the option to simulate is still disabled.

Screenshot 2024-12-13 at 9 59 23 AM Screenshot 2024-12-13 at 9 59 17 AM
@andreaskatis
Copy link
Contributor

Hi Tyler,

I will need a bit more information for this. Do you have NuSMV installed and if yes, are you able to access the simulator from the requirements editor? An easy way to see this is to open any requirement in the requirement editor, click on the SEMANTICS button, then see if the SIMULATE button is enabled in the bottom of the Assistant tab. I'm attaching a screenshot below.

image

@smithdtyler
Copy link
Author

After installing NuSMV and LTLSIM, the Simulate button was in the requirement editor was enabled (see #103 for a recommendation for documentation regarding LTLSIM)

After confirming the simulate option in the requirement editor worked, I returned to the realization analysis tool. After switching to JKind and checking realizability, the simulate action was enabled.

However, the tool tip was stale (see screenshot), I opened #104 accordingly.

Screenshot 2024-12-13 at 11 19 47 AM

@smithdtyler
Copy link
Author

After the help from @andreaskatis I am now able to run simulation. Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants