Incorrect Verification Result for Property Type 2
Atefeh-Zareh opened this issue · 3 comments
Issue Description:
When defining properties of the second type in the VeriSolid design application and analyzing the smart contract, an issue arises where the tool provides an incorrect verification result. Specifically, let's consider the "RockPaperScissors" smart contract which is a predefined smart contract. The issue happens to the property "close#cancelPlay," which asserts that the event "(close)" can happen only after the event "(cancelPlay)." The tool's output result suggests that this property holds, despite visual expectations indicating otherwise. To provide visual context and clarity, the "RockPaperScissors" smart contract image that is provided in the following, illustrates the relationship between "(close)" and "(cancelPlay)" events in the "RockPaperScissors" contract. The image clearly demonstrates that the property "close#cancelPlay" should not hold based on the contract's behavior.
Steps to Reproduce:
- Open the VeriSolid design application.
- Load the "RockPaperScissors" contract example.
- Define a property of the second type: "close#cancelPlay."
- Click on Run.
- Observe the verification result output in the "/smart-contracts/projectOutputs/" folder.
Expected Behavior:
Given the nature of the "RockPaperScissors" contract and the property "close#cancelPlay," it is expected that the verification result would indicate that the property does not hold. The logical relationship between "(close)" and "(cancelPlay)" events implies that "(close)" should not be able to occur only after "(cancelPlay)."
Actual Behavior:
The verification result output suggests that the property "close#cancelPlay" holds, contrary to expectations. The output states that the specification property is true.
"-- (close) can happen only after (cancelPlay) --
-- specification A [ !(BAUC_aclose_guard) U BAUC_acancelPlay_guard ] is true
system diameter: 8
reachable states: 23 (2^4.52356) out of 3.85876e+09 (2^31.8455)"
Additional Information:
The main reason for this issue is translating the CTL logic into NuXmv and "weak until" is defined wrong.
Contributor's Note:
I will address this issue by providing the necessary code changes to correct the verification discrepancy. The objective is to enable the VeriSolid tool to accurately determine the validity of the specified property. Anticipating the acceptance of the pull request, I aim to enhance the tool's reliability and analysis capabilities through the resolution of this concern.
Hi @Atefeh-Zareh, Thanks for creating this issue! Can you provide more explanations on this part:
"The main reason for this issue is translating the CTL logic into NuXmv and "weak until" is defined wrong."
Thanks,
Anastasia
Hi Anastasia,
Thank you for your prompt response and for considering my issue registration. I appreciate your willingness to address this issue. To provide more detailed explanations:
Property 2 in the VeriSolid paper is defined as "p can happen only after q," and its corresponding CTL formula is declared as "A[!p W q]." As you correctly pointed out, NuXmv does not support "weak until" directly, which necessitates a translation of this CTL formula into NuXmv-compatible syntax. Currently, this translation is done using an "until" syntax in the generateSecondTemplateProperties link and "FAIRNESS" in generateSecondTemplateFairnessProperties link functions. This results in the following statements in the NuXmv output file:
CTLSPEC A [ !property[0] U property[1]]
FAIRNESS (property[0]);
The root of the issue lies in this NuXmv translation because it does not faithfully represent the targeted CTL formula "A[!p W q]" (where p and q in the paper correspond to property[0] and property[1] in the Git code).
According to the NuXmv User Manual, FAIRNESS is supported from NuSmv for backward compatibility, and its meaning, based on the NuSmv Tutorial, is: "A fairness constraint restricts the attention of the model checker to only those execution paths along which a given formula is true infinitely often." While FAIRNESS has its uses, it does not align with the semantics required for the "weak until" definition. I would greatly appreciate it if you could clarify whether my understanding of the code's use of FAIRNESS is accurate or if there's a different purpose for its inclusion.
In the proposed code correction in pull request #10, the following relationship between "until" and "weak until" is employed:
A[ f W g] = ! E[!g U (!f & !g)]
This equivalence is also available in this reference (5th page). In the context of the Git code, this results in the following CTL formula:
CTLSPEC ! E[!(property[1]) U (property[0] & !(property[1]))]
I would also like to invite you to consider the counterexample explained in the issue description. It appears that this counterexample is not detected in the current state of the Git master branch code, but the code suggested in pull request #10 correctly identifies the property violation. This further supports the need for the proposed code correction.
Once again, thank you for your dedication to open-source development and your willingness to address this issue. If you require any additional clarifications or have further questions, please do not hesitate to reach out.
Best,
Atefeh