CIF explorer: generate state annotations on locations of state space automata

The CIF explorer computes a state space and can output it as a CIF model, with a single automaton and a location per state of the state space. The CIF explorer stores all the information of the states internally, but only the states and transitions become locations and edges. The contents of the states are lost. By adding state annotations to the locations, the contents of the state would be available. This way, users can inspect the models more easily, and more easily link states from the state space back to the original specification. By using annotations, tools could also process the annotations from the state space.