Debug/Analyze does not correctly highlight unrealizable cores

[wongkaiweng]

I got the following highlight (with LTLMoP/development)

but I think it should be (with vramen/cores)

I can also obtain the same result with the following replacement in specEditor.py:

FROM
#highlight guilty sentences
#special treatment for goals: we already know which one to highlight
if self.proj.compile_options["parser"] == "structured":
for h_item in self.to_highlight:
tb_key = h_item[0].title() + h_item[1].title()
if h_item[1] == "goals":
self.text_ctrl_spec.MarkerAdd(self.tracebackTree[tb_key][h_item[2]]-1, MARKER_LIVE)
elif self.proj.compile_options["parser"] == "slurp":
for frag in self.to_highlight:
tb_key = frag[0].title() + frag[1].title()
self.text_ctrl_spec.MarkerAdd(self.tracebackTree[tb_key][frag[2]]-1, MARKER_LIVE)
self.analysisDialog.markFragments(*frag)
else:
print "Fragment marking not yet supported for this parser type"

TO (copied from varmen/cores' branch)
if not realizable or not nonTrivial:
#only do cores if unrealizable or trivial

            #highlight guilty sentences
            #special treatment for goals: we already know which one to highlight                
            for h_item in self.to_highlight:
                tb_key = h_item[0].title() + h_item[1].title()
                if h_item[1] == "goals":
                    self.text_ctrl_spec.MarkerAdd(self.tracebackTree[tb_key][h_item[2]]-1, MARKER_LIVE)

            if self.unsat:
                guilty = compiler._coreFinding(self.to_highlight, self.unsat, self.badInit)
                self.highlightCores(guilty)
            else:
                #just highlight all sentences in the guilty components
                for h_item in [h for h in self.to_highlight if h[1] != "goals"]:
                        tb_key = h_item[0].title() + h_item[1].title()
                        for l in self.tracebackTree[tb_key]:
                            self.highlight(l, h_item[1])
    """

[cfinucane]

A couple of things:

1. vraman/cores is deprecated. All relevant commits have been merged into development. @vraman, would you mind to maybe delete it if you're not using it anymore? :)
2. The non-cores analysis, which is what you've run here, highlights only the affected goal (to accompany the text "System highlighted goal unrealizable: 0"). Therefore, this is the expected behavior (I believe).
3. The button below the output text in the "Analysis Results" window is what would normally say "Refine analysis..." and let you run core-finding to get better highlighting. It is disabled in this case because it is under-tested and therefore currently disabled by default in the case of an unrealizabile spec (as opposed to unsat, in which case it shows). If you want to play with it, you can modify the condition here: https://github.com/LTLMoP/LTLMoP/blob/development/src/specEditor.py#L1408
4. Core-finding was developed mostly in conjunction with SLURP, so the highlighting in the core-finding case when using Structured English does in fact appear to be broken, but you can still see the raw LTL output in the terminal. I will look into making the highlighting work before closing this issue.

[cfinucane]

Oh, and 5:

This specific example returns for me:

set(['\t\t\t []<>( ((!s.bit0 & !s.bit1 & !s.bit2))) ', '!e.fire & e.person & !s.radio & !s.bit2 & s.bit1 & !s.bit0 & next(e.fire) & next(!e.person)', '!e.fire & !e.person & !s.radio & !s.bit2 & s.bit1 & !s.bit0 & next(e.fire) & next(!e.person)', 'e.fire & !e.person & !s.radio & !s.bit2 & s.bit1 & !s.bit0 & next(e.fire) & next(!e.person)', '!e.fire & e.person & !s.radio & s.bit2 & !s.bit1 & s.bit0 & next(e.fire) & next(!e.person)', ' []( ((!s.bit0 & !s.bit1 & !s.bit2)) -> ( ((!next(s.bit0) & !next(s.bit1) & !next(s.bit2)))| ((!next(s.bit0) & next(s.bit1) & next(s.bit2))) | ((next(s.bit0) & !next(s.bit1) & !next(s.bit2))) ) ) & []( ((!s.bit0 & !s.bit1 & s.bit2)) -> ( ((!next(s.bit0) & !next(s.bit1) & next(s.bit2)))| ((!next(s.bit0) & next(s.bit1) & next(s.bit2))) | ((next(s.bit0) & !next(s.bit1) & !next(s.bit2))) ) ) & []( ((!s.bit0 & s.bit1 & !s.bit2)) -> ( ((!next(s.bit0) & next(s.bit1) & !next(s.bit2)))| ((next(s.bit0) & !next(s.bit1) & !next(s.bit2))) | ((next(s.bit0) & !next(s.bit1) & next(s.bit2))) ) ) & []( ((!s.bit0 & s.bit1 & s.bit2)) -> ( ((!next(s.bit0) & next(s.bit1) & next(s.bit2)))| ((!next(s.bit0) & !next(s.bit1) & !next(s.bit2))) | ((!next(s.bit0) & !next(s.bit1) & next(s.bit2))) | ((next(s.bit0) & !next(s.bit1) & next(s.bit2))) ) ) & []( ((s.bit0 & !s.bit1 & !s.bit2)) -> ( ((next(s.bit0) & !next(s.bit1) & !next(s.bit2)))| ((!next(s.bit0) & !next(s.bit1) & !next(s.bit2))) | ((!next(s.bit0) & !next(s.bit1) & next(s.bit2))) | ((!next(s.bit0) & next(s.bit1) & !next(s.bit2))) ) ) & []( ((s.bit0 & !s.bit1 & s.bit2)) -> ( ((next(s.bit0) & !next(s.bit1) & next(s.bit2)))| ((!next(s.bit0) & next(s.bit1) & !next(s.bit2))) | ((!next(s.bit0) & next(s.bit1) & next(s.bit2))) ) ) ', 'e.fire & !e.person & !s.radio & s.bit2 & !s.bit1 & s.bit0 & next(e.fire) & next(!e.person)'])

which is... not what we want. It appears to contain (a) the offending goal, (b) the topology, and (c) every valid initial state. Aaand thus why the code is disabled pending further evaluation :)

[vraman]

Additional related issue: analyzing examples/unsynth/unsynth_simple (refined analysis) gives the following error:

Traceback (most recent call last):
File "specEditor.py", line 184, in onClickRefineAnalysis
self.parent.refineAnalysis()
File "specEditor.py", line 1455, in refineAnalysis
guilty = self.compiler._coreFinding(self.to_highlight, self.unsat, self.badInit)
File "/Users/Vasu/Documents/LTLMoP/src/lib/specCompiler.py", line 655, in _coreFinding
aut = fsa.Automaton(proj_copy)
AttributeError: 'module' object has no attribute 'Automaton'

This seems to stem from modifications to fsa.py.

[spmaniato]

@vraman This latest issue is similar to #71, i.e., a result of the latest changes in development (refactoring, strategy, etc). Cameron is working on it.

[wongkaiweng]

I have updated the Refine Analysis part to work with the latest fsa.py and strategy.py. It is committed to 8f65fe1. The branch is called upstream/update_cores_to_strategy. I'm not sure whether the core part is working but it will finish the analysis.

You can also take a look at 8085cf1. The branch is called cfinucane/modern_cores and it has a version of the core analysis.