The format of files containing Kripke structures has been clarified. The clarification is "there may be one or more lines beginning with “Transitions” that identify transitions. Similarly, there may be one or more lines beginning with “Label.” Each “Label” line contains one state and a list of atomic proposition (AP) labels for that state. No white space in strings used as APs, no commas between transition pairs an white space is ok everywhere else."
[Project 1 Description (from syllabus)]