GitHub - akaydesai/mcsv-LTL: Simple bounded model checker for LTL(Linear Temporal Logic). (as part of Model Checking and Software Verification coursework.).

akaydesai / mcsv-LTL Public

Notifications You must be signed in to change notification settings
Fork 0
Star 1

Simple bounded model checker for LTL(Linear Temporal Logic). (as part of Model Checking and Software Verification coursework.).

View license

1 star 0 forks Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 1 Commit
LICENCE		LICENCE
README		README
checks.py		checks.py
debug_dump.py		debug_dump.py
formulas.py		formulas.py
input.py		input.py
main.py		main.py
parser.out		parser.out
parsetab.py		parsetab.py
ply_label_lexer.py		ply_label_lexer.py
ply_label_parser.py		ply_label_parser.py
ply_lexer.py		ply_lexer.py
ply_parser.py		ply_parser.py

Repository files navigation

Open input.py to provide input. 
Then run main.py

input.py includes the following example transition system as input.

init state is 00
Transitions:
00 -> 10
10 -> 11
10-> 01
01 -> 00
11 -> 00

As formula: ((((!x1.!x0).(x1'.!x0'))+((!x1.x0).(!x1'.!x0')))+(((x1.x0).(!x1'.!x0'))+((x1.!x0).((x1'.x0')+(!x1'.x0')))))

Simple testcases for the above transition system, which is already included in input.py are given below:

( _P_ U _Q_) is valid.
X x0 is not valid.
( _P_ U _R_) is not valid.
F _R_ is not valid
F _Q_ is valid.
G _S_ is valid.

_P_, _Q_ etc are labelling predicates, which have been defined in input.py. You can replace those with your own.

Read input.py for more details.