Skip to content

Aurele-Barriere/CTLSKD_MC

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

36 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

CTL*KD Model-Checker

Put the executable NuSMV in src/, then type make.
This generates mc.out, which tests all model-checkers.

make tests also builds 3 executable for testing ltl, ctls and ctlskd model-checking.
These executable take 2 arguments: size of the formula and size of the model to generate.

About

A model-checker for CTL*KΔ

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages