Re: [isabelle] Nitpick Codatatype - No Counterexample found



Dear Sebastian,

Sorry for the delay in answering. Investigating Nitpick failures is tricky, especially that I developed the tool over 10 years ago.

I wasn't quite able to put my finger on the deep problem -- perhaps simply an issue in the translation from HOL terms to first-order relational logic (Kodkod's logic), which is optimized and hence quite subtle. However, while investigating the issue, I rephrased one of the codatatype constraints, hoping this would make the problem go away, and it did (at least with the "box" option on). This is not entirely satisfactory, but my middle-term goal is to replace Nitpick with the experimental Nunchaku, so I don't want to spend too much time on Nitpick.

If you wonder, the issue seems to be that the (lazy) lists [a] and [a, a] are considered bisimilar even if they are not. The bisimilarity check has a depth (bisim_depth), and indeed with bisim_depth = 1 we'd expect [a] and [a, a] to be identical. But here we're working with bisim_depth = 2, and hence they're different and thus it should be possible to construct a model that contains both. (The list [a] is needed to build [a, a], so it's unavoidable in a model.)

Cheers,

Jasmin

On 26 Feb 2021, at 11:36, Stüber, Sebastian <stueber at se-rwth.de> wrote:

Dear all, 
I am trying to use nitpick to find counterexample over (potentially) infinite lists. While playing with nitpick I encountered a strange behavior:
    Nitpick seems to be unable to find counterexamples, if a message occurs twice in the list
 
An Example:
 
codatatype 'a::type llist = LNil | LCons 'a "'a llist"
 
(* Notice that "a" occurs twice *)
lemma "LCons (a::nat) (LCons a LNil) ≠ z"
  nitpick[expect=none]  (* Should find something! *)
  oops
 
 
(* Allowing different messages, now nitpick can find something *)
lemma "LCons (a::nat) (LCons b LNil) ≠ z"
  nitpick[expect=genuine]   (* is working *)
  oops
 
 
With the normal (finite) list datatype, this problem does not occur.
 
Does anybody know the cause & how to fix it?
 
Sincerely,
Sebastian Stüber
 
 
---------------------------------------------------------------
Sebastian Stüber, M.Sc.RWTH           |    Software Engineering
Lehrstuhl für Software Engineering    |  RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany   |  https://www.se-rwth.de
Phone ++49 241 80-21352          
 
 
 
<nitpick_test.thy>



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.