pettni / arcs Goto Github PK

https://github.com/pettni/abstr-refinement/blob/d6aa68810a5c10ad0f14b5248123d2ce3d23ae29/abstr-ref/%40TransSyst/win_dual.m#L39

The current pre function only takes boolean values as its quant inputs. For the line above, 'forall' will be interpreted as true, that is 'exists', in pre.

Not sure for this line the 'forall' is a typo of 'exists', or should be replaced with false.

'win_eventually_or_peresistence.m':

1. There is no values assigned to output 'C'.
2. Line 17,18,27,28: the index seems to be 'end+1' instead of 'end'. Otherwise, 'Vlist' and 'Klist' are initialized as empty matrices, where the index 'end' is unavailable.

'Controller.m':

1. A error appears when calling 'get_input'and the method visits a sub-controller corresponding to a progress group. I guess the reason is that the set V and an empty controller is always added as the first term when the sub-controller for progress group is generated.
2. Line 75 in 'Controller.m': why not directly search the sets containing that state and find out the one with smallest number instead of using the one before current ('bottom_cnt.mem_var-1') ?

It might be too much overhead to write all the info about the process on the screen (I'm refering to radiant_BDD example). Might make sense to have a verbose flag to silence it.

https://github.com/pettni/abstr-refinement/blob/685cf194a2b7d794fe09ba577fb87d04cd7ef8d8/abstr-ref/%40TransSyst/win_primal.m#L72-L73

Hi Peter (@pettni) ,
I am confused about the two lines above. Why don't we need to save the controllers returned by Pre and PGPre here? There is usually a gap between Z and V. I thought that the controller for Pre(V) might be contained by the controller of win_intermediate in the next few lines. But today I encounter some issues when executing the controller returned by the win_primal, which I think might be relevant to my question here. Could you please help me find the answer?

Thank you,
Zexiang

It only implements the inheritance part but does not take advantage of the possibility of new progress groups emerging after partitioning.

plot(part.cell_list([]))

fails with the error:

Error using  > 
Not enough input arguments.

Error in Rec/plot (line 51)
    if rec.dim>3

Essentially, plot(part) fails when there is no part with empty AP. I'll post an update if I can fix it.