hahn icon indicating copy to clipboard operation
hahn copied to clipboard
verified publisher icon vafeiadis

Incorrect state index in LTS_complete_trace ?

Open InnocentusLime opened this issue 1 year ago • 1 comments

It seems that the index given to the LTS_final predicate is incorrect in HahnTrace, line 733.

If I am not mistaken, LTS_final is used to denote the terminal state. However LTS_complete_trace requires state 0 to be terminal. It is not obvious why it should be this way.

InnocentusLime avatar Feb 07 '24 11:02 InnocentusLime

You are right: the index should be length l.

vafeiadis avatar Feb 07 '24 11:02 vafeiadis