Open numairmansur opened 7 years ago
As expected from the behaviour of [WP() for Havoc](https://github.com/numairmansur/Error-Localization/wiki/Weakest-Precondition-operator-WP()) WP(z>10; havoc z)
returns false
.
and hence all the assignment statements in the trace, before havoc are not relevant.
The implementation works as it should. I think we need to modify the definition of relevancy a little in our original document. Form the document, we define restrictiveness and relevancy as follows:
But i think we should mention that the assignment statement is relevant if replacing this assignment with havoc causes some assume statement to become restrictive which was not restrictive in the original trace.
The new definition of Relevancy should be:
Thanks for the detailed analysis. This is definitely a step in the right direction, but it is not sufficient. I added an example to demonstrate the problem. We probably need something to measure the "amount" of restrictiveness. Maybe we can do this by defining something like a "blocking execution" and by comparing the set of blocked executions before and after replacing assignments by havoc.
Error Trace
"y := 42;" "havoc x;" "assume x >= 0 && y >= 23;" "assume !false;"
Output on Ultimate:
[L16] * y := 42;
VAL [y=42]
[L17] @ havoc x;
VAL [y=42]
[L18] - assume x >= 0 && y >= 23;
VAL [x=0, y=42]
[L19] - assert false;
VAL [x=0, y=42]
Hi @Heizmann and @schillic I was working on a formal definition of a blocking execution and a set of blocking executions. But a problem hit my mind. It is possible that the error trace might already have infinite blocking executions before we replace the assignment with havoc. After replacing the assignment with havoc we might have more blocking executions but it will still be infinite. in that case does it make sense to compare the two sets of infinite blocking executions ? Because i was thinking to declare x:=t relevant if after replacing x:=t with havoc, the set of blocking executions before the replacement is smaller then the set after.
Why would infinity be a problem? Just do not say "|A| < |B|" but say "A is a strict subset of B" ("A \subsetneq B").
Ok yes that makes sense. I don't know why i was thinking in terms of the size of the two sets.
Hi @Heizmann @schillic
What do you think of the new definition for relevancy?
Please let me know if you think something is missing or not making sense. Or if something requires more clarification.
This is conceptually very good, I think this is exactly the definition that we need. (I am sometimes too optimistic, Christian is much better in finding Problems.)
Maybe the term blocking executions is misleading. Should we call it blocked execution?
Let \pi' represent the trace (not a trace).
Since this is an important definition, we should be more verbose here. E.g., as follows. We say that the assignment statement \pi[i] is relevant if the trace after the replacement has strictly more blocked executions than the trace before the replacement, i.e., if \beta \subsetneq \beta' (Use \subsetneq instead of \subset)
I agree with @Heizmann with a few extra comments (not all of them important).
In the intro the index of the statement fits the index of the predecessor state (i.e., you have triples (s_i, tf(pi[i]), s_{i+1})). However, in the definition Blocking Execution you say s_{j-1} does not imply guard(pi[j]). Is this intentional? Then I do not understand it.
If the above was a typo and s_{j-1} should be s_j, then there is a contradiction between s_j, s_{j+1} |= tf(pi[j]) (intro) and s_j does not imply guard(pi[j]) (Blocking Execution) because tf(pi[j]) implies guard(pi[j]).
I think we can keep the definition of a Blocking Execution on a more general level and not talk about assume statements at all but instead only talk about transition formulas. In a simple language the only transition formula that has a nontrivial condition is the assume statement. But in the general case in Ultimate we have statements that are a combination of assume, assignment, and havoc statements and the definition could still make sense.
I would not use lowercase letters for sets (epsilon, beta), even with Greek letters. (The capital version of epsilon and beta look like the Latin letter.) Moreover, I would prefer to turn the sets into functions that take the trace as an argument. In that case I would rather rename them to exec(pi) and block(pi) (or Exec/Block).
Regarding 3. I think that lifting all these definitions from statements to transition relations (the TransFormulas in Ultimate) is a separate task. That task should be done for all our definitions and theorems, but I think we also want to have a version of all defintions/theorems for statements. (We do not want both versions in the paper, but I think we need both versions in order to understand better what we are doing)
Hi @schillic , regarding your concerns in
Yes you are right, it should be s_j. In the following example, in the case of j = 4, for \pi[4], sj to s {j+1} should be s_4 to s_5.
I see what you mean here. I have modified the definition a little, what do you think about it now.
Noted. I am adding this as a separate new task.
But the reason i used sets is because i wanted to say in the end that the assignment is relevant if \beta \subsetneq \beta'. Why do you think turning the sets into functions would be better ?
Yes, it looks good now.
What I meant was a function that takes a trace and produces a set of executions. This is only a matter of taste, it is equivalent saying "let epsilon bei the executions of pi" and "epsilon(pi)".
havoc(x) is relevant if there exists an assignment x:=t, such that if we replace that havoc with that assignment then all executions of \pi' are blocking (\pi' is infeasible).
Hi @Heizmann @schillic,
So, here is the example on which our new definition of relevancy does not work.
y :=10 ; havoc(x) ; assume(x>10)
So, if we consider the statement y:=10
,according to our definition it would be relevant because changing it to havoc gives us more blocking executions. But obviously it should not be relevant here.
Please note that if we check it formally with our mathematical formulas and our implementation then it is not relevant. The problem arise in this example only because of how we are defining relevancy with the help of number of blocking executions.
Hi @Heizmann @schillic What do you think ?
I think the term infeasible execution is not good. Either there is an execution or there is no execution. I think the old definition of a blocked execution is ok. I need more time to think about Definition 3.
Ok. I changed the term "infeasible" with "blocked" in the above comment :)
I think the point of @Heizmann was to use the old definition.
About Def. 3:
Hi @schillic Regarding point 3. Yes that is no problem. Those blocking executions are still there and it is no problem if there already are blocking executions. What we are interested in is the new blocking execution(s) which was introduced because there is a new state in Q' \ Q which is now reachable from P if we change x:=t to havoc(x).
You never said that the new state is in Q' \ Q. But more importantly, the definition is too complicated if we write it like this.
Oh yes you are right. Ok i am updating it.
But are you really sure that every execution that start in state s'_i+1 which is in (Q' \ Q) will be blocking ? I think not every execution will be blocking but there exists at least one state for which we will get a blocking execution.
It is possible that every execution might be blocking but i think we cannot say that this will always be the case. I think even if there is one more blocking execution, then that is good enough for us to declare the assignment statement relevant.
Q is the error precondition of the suffix trace. That means all states not in Q have only blocking executions for that trace.
Oh yes i see. You are right.
Another version of the definition that @Heizmann and I were discussing just now:
Let pi = "st_1, ..., st_i-1, x := t, st_i+1, ..., st_n" be an error trace of length n.
The assignment at position i is relevant if there is an execution s_1, ..., s_n+1 of pi and some value v such that every execution of the trace "x := v, st_i+1, ..., st_n" starting in s_i is blocking.
And a generalization that also works for the havoc case:
Let pi = "st_1, ..., st_n" be an error trace of length n where st_i is an assignment statement or a havoc statement that assigns a new value to variable x.
The statement at position i is relevant if there is an execution s_1, ..., s_n+1 of pi and some value v such that every execution of the trace "x := v, st_i+1, ..., st_n" starting in s_i is blocking.
Hi @schillic, in the definition
The assignment at position i is relevant if there is an execution s_1, ..., s_n+1 of pi and some value v such that every execution of the trace "x := v, st_i+1, ..., st_n" starting in s_i is blocking.
Why do we have to say _if there is an execution s_1, ..., sn+1 of pi . Do you mean here that the error trace should be feasible ?
Even more: "havoc(x); assume(x == 1)" is feasible, but we are interested in an execution that "goes through".
I see.
is it also the same if i replace the last line as following:
"The assignment at position i is relevant if there is an execution s_1, ..., sn+1 of pi and some value v such that the trace "x := v, st_i+1, ..., st_n" is infeasible._ "
Am i wrong in thinking that for the trace x := v, st_i+1, ..., st_n
, it dosen't matter from which state we begin the execution, we will always get a blocking execution ?
No, the state s_i matters (not for x but for the other variables). Take the trace "y := 0; x := 1; assume(x != y)". After replacing x := 1 by x := 0 the whole trace is infeasible. But the subtrace "x := 0; assume(x != y)" is still feasible, depending on the state where you start.
oh yes that is a good example ! ok now i think i also agree with the definition. So i will write it down and modify the proof and let you know if i have questions :)
So here is the updated document. Can you take a look at the proof :)
Consider the following program:
With the following error trace.
"x := 1;", "y := 2;", "z := 3;" , "havoc z;" , "assume !(z > 10);"
Below i show the error trace with it's weakest precondition list.
Output on Ultimate