search

vafeiadis / hahn

Hahn: A Coq library
MIT License
29 stars 15 forks source link

Incorrect state index in LTS_complete_trace ? #33

Open InnocentusLime opened 8 months ago

InnocentusLime commented 8 months ago

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.

vafeiadis commented 8 months ago

You are right: the index should be length l.