Skip to content
Snippets Groups Projects
Commit c796811b authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Do no try to create a trace from an initial state.

[Bug][TLC]
parent dd7ff0b8
No related branches found
No related tags found
No related merge requests found
......@@ -77,6 +77,10 @@ public class ConcurrentTLCTrace extends TLCTrace {
* @see TLCTrace#getTrace(LongVec)
*/
public TLCStateInfo[] getTrace(final TLCState state) throws IOException {
if (state.isInitial()) {
return new TLCStateInfo[] {new TLCStateInfo(state)};
}
final LongVec fps = new LongVec();
// Starting at the given start fingerprint (which is the end of the
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment