Hello Daniel,
Than you very much, you are absolutely right. I am changing abstract variables. Now I specified the refinement in event cas and everything works fine.
Best regards,
André Passos.
On Nov 29, 2012, at 7:49 PM, Daniel Plagge wrote:
> Hello again,
>
> I just read your first email. Based on the screenshot, it looks like all variables "searched", "lt" and "rt" are already present in the abstract model "Processes" and "cas" does not refine any event. So it is not allowed to change any of these variables. Maybe you have just forgotten to specify which event cas refines?
>
> Best regards
> Daniel
>
> Am 29.11.2012 20:42, schrieb Daniel Plagge:
>> Hello André,
>>
>> ProB found an error in an event ("cas"). I have to admit that the "explanation" is very hard to understand. It seems that the event assigns a new value to a variable that must not be modified because its abstract event does not modify that variable. There should be an unproven proof obligation "cas/x/EQL" where x is some variable that is modified by cas (I guess it's "searched", "lt" or "rt").
>>
>> If this is not the case, could you please send me your model if it's not confidential? (Directly to my address, not to the list.)
>>
>> One problem (beside being hard to understand) is that the last part of the error message reveals a bug in ProB ("no rule to explain event step invalid_modification"). It is unable to print what exactly failed.
>>
>> ProB "executes" the event starting with the concrete part to the abstract part and in case it finds an error, it shows a trace of the computation steps:
>>
>>> [...]
>>> Event cas in model CompareAndSwap:
>> First it finds solutions for the parameters that fulfil the guards:
>>>
>>> for the parameters:
>>> e = 1
>>> l = locks3
>>> p = processes2
>>> r = tl
>>> the guard is true:
>>> p : searched
>>> & r : nodes \ {hd}
>>> & (r /= tl => key(r) >= gkey(p))
>>> & l : nodes \ {tl}
>>> & (l /= hd => key(l) < e)
>>> & (next(l) /= tl => e < key(next(l)))
>>> & gkey(p) = e
>>> & next(l) = r
>>> & (lt(p) /= l or rt(p) /= r)
>>>
>> It executes each action of the event with the found parameters:
>>> executing an action:
>>> searched := {}
>>>
>>> executing an action:
>>> lt := {}
>>>
>>> executing an action:
>>> rt := {}
>> And then checks if a variable has been modified that must not be modified. But here we encounter a bug: The pretty-printer that should put the trace into a human-readable format has no rule to print this kind of step in the trace. I have created a ticket in the ProB bug tracker.
>>>
>>> (no rule to explain event step invalid_modification)
>>>
>>> Does anyone know what this means?
>>>
>>
>> I hope that I was able to make it clearer. Thank you for your report, André.
>>
>> With best regards
>> Daniel
>>
>>
>>
>>
>>> Thanks in advanced.
>>>
>>> Best regards, André Passos.
>>>
>>>
>>> ------------------------------------------------------------------------------
>>> Keep yourself connected to Go Parallel:
>>> VERIFY Test and improve your parallel project with help from experts
>>> and peers. http://goparallel.sourceforge.net
>>>
>>>
>>> _______________________________________________
>>> Rodin-b-sharp-user mailing list
>>> Rodin-b-sharp-user@...
>>> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
>>
>>
>>
>> ------------------------------------------------------------------------------
>> Keep yourself connected to Go Parallel:
>> VERIFY Test and improve your parallel project with help from experts
>> and peers. http://goparallel.sourceforge.net
>>
>>
>> _______________________________________________
>> Rodin-b-sharp-user mailing list
>> Rodin-b-sharp-user@...
>> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
>
> ------------------------------------------------------------------------------
> Keep yourself connected to Go Parallel:
> VERIFY Test and improve your parallel project with help from experts
> and peers. http://goparallel.sourceforge.net_______________________________________________
> Rodin-b-sharp-user mailing list
> Rodin-b-sharp-user@...
> https://lists.sourceforge.net/lists/listinfo/rodin-b-sharp-user
|