By using PAT model checker, we can create a mAskodel and simulate it, so for verifying a CTL specification for model, we should translate this model to SMV code that verify it in NuSMV model checker.
Hello,
We developed a JAVA transformation tool that accepts ,as input, any model and translates it into NuSMV code. Please check the following link.
https://github.com/Marooned202/jtl.
I'd say that it is perhaps beter to wrap nusmv as an extension to PAT; afterall PAT is built to be extensible. Do you really need CTL? Or can you do it with LTL, which is supported by PAT?
Hello
dear Dr failsal
when i download JTL-master, i can not open Main.java how can i fixed it?
dear Wishnu Prasetya
i want compare a system using two model checkers NuSMV and PAT
there after, i want PAT model translate to NuSMV for verifying CTL specifications
Hello,
You just simply create a JAVA project in your machine and copy the required classes then run the main.java. It should work.
Regards,
- Badges
- Science topic