Does anyone have code for Four-Knights Puzzle written in smv (nusmv or nuxmv)? I describe the problem with a grid, but when I tried to write the constraints/moves, I got errors like:
line 35: recursively defined: S1
in definition of next(S3) at line 43
in definition of next(S1) at line 35
I understand this issue but don't know how can I implement this problem and avoid this recursively.
Thanks!
well, finally I succeeded on my own (I implemented a winning strategy for the black, for the situations in which he must have won):
LTL check (0 meaning the black is the winner):
and got:
-- specification F (vec = 0 & player = B) is true