Project

General

Profile

Bug #13

Wrong CL result

Added by Thorsten Wißmann over 3 years ago. Updated over 3 years ago.

Status:
Closed
Priority:
Normal
Start date:
05/09/2014
Due date:
% Done:

100%


Description

The formula ([1,3] C) ∧ ([2,3] ¬C) should be satisfiable but coalg says:

$ ./coalg.native sat CL <<< '([{1 3}] C) & ([{ 2 3 }] ~C )'

Formula 1: unsatisfiable


Subtasks

Bug #14: Strange CL resultClosed

History

#1 Updated by Thorsten Wißmann over 3 years ago

  • Status changed from New to In Progress

Tatl claims the formula to be satisfiable. Running

./tatl-compatibility-wrapper.sh <<< '([{1 3}] c) & ([{ 2 3 }] ~c )'

gives the output:
         ----------------------------------------------
         |           TATL : Tableaux for ATL          |
         |          Amelie David - Lab. IBISC         |
         |     23 bd de France -  91037 Evry Cedex    |
         ----------------------------------------------

*
* The formula is satisfiable.
*

*
* Pre-tableau 
**************

P0: ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p)
   Succ: S1
P1: ~~c
   Succ: S6
P2: ~~~c
   Succ: S5
P3: T
   Succ: S4
P4: p\/~p
   Succ: S2 ; S3
S1 (Consistant) : ~<<1,3>>X~c ; ~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p) ; <<1,2,3,4,5>>X(p\/~p)
   Succ: (0,1,0,1,2)(0,1,0,2,1)(0,1,1,1,2)(0,1,1,2,1)(0,1,2,1,1)(0,1,2,2,2)(0,2,0,1,1)(0,2,0,2,2)(0,2,1,1,1)(0,2,1,2,2)(0,2,2,1,2)(0,2,2,2,1)(1,1,0,1,2)(1,1,0,2,1)(1,1,1,1,2)(1,1,1,2,1)(1,1,2,1,1)(1,1,2,2,2)(1,2,0,1,1)(1,2,0,2,2)(1,2,1,1,1)(1,2,1,2,2)(1,2,2,1,2)(1,2,2,2,1)(2,1,0,1,1)(2,1,0,2,2)(2,1,1,1,1)(2,1,1,2,2)(2,1,2,1,2)(2,1,2,2,1)(2,2,0,1,2)(2,2,0,2,1)(2,2,1,1,2)(2,2,1,2,1)(2,2,2,1,1)(2,2,2,2,2)->P1 ; (1,0,0,1,1)(1,0,0,2,2)(1,0,1,1,1)(1,0,1,2,2)(1,0,2,1,2)(1,0,2,2,1)(1,1,0,1,1)(1,1,0,2,2)(1,1,1,1,1)(1,1,1,2,2)(1,1,2,1,2)(1,1,2,2,1)(1,2,0,1,2)(1,2,0,2,1)(1,2,1,1,2)(1,2,1,2,1)(1,2,2,1,1)(1,2,2,2,2)(2,0,0,1,2)(2,0,0,2,1)(2,0,1,1,2)(2,0,1,2,1)(2,0,2,1,1)(2,0,2,2,2)(2,1,0,1,2)(2,1,0,2,1)(2,1,1,1,2)(2,1,1,2,1)(2,1,2,1,1)(2,1,2,2,2)(2,2,0,1,1)(2,2,0,2,2)(2,2,1,1,1)(2,2,1,2,2)(2,2,2,1,2)(2,2,2,2,1)->P2 ; (0,0,0,0,1)(0,0,0,0,2)(0,0,0,1,0)(0,0,0,1,1)(0,0,0,1,2)(0,0,0,2,0)(0,0,0,2,1)(0,0,0,2,2)(0,0,1,0,0)(0,0,1,0,1)(0,0,1,0,2)(0,0,1,1,0)(0,0,1,1,1)(0,0,1,1,2)(0,0,1,2,0)(0,0,1,2,1)(0,0,1,2,2)(0,0,2,0,0)(0,0,2,0,1)(0,0,2,0,2)(0,0,2,1,0)(0,0,2,1,1)(0,0,2,1,2)(0,0,2,2,0)(0,0,2,2,1)(0,0,2,2,2)(0,1,0,0,0)(0,1,0,0,1)(0,1,0,0,2)(0,1,0,1,0)(0,1,0,1,1)(0,1,0,2,0)(0,1,0,2,2)(0,1,1,0,0)(0,1,1,0,1)(0,1,1,0,2)(0,1,1,1,0)(0,1,1,1,1)(0,1,1,2,0)(0,1,1,2,2)(0,1,2,0,0)(0,1,2,0,1)(0,1,2,0,2)(0,1,2,1,0)(0,1,2,1,2)(0,1,2,2,0)(0,1,2,2,1)(0,2,0,0,0)(0,2,0,0,1)(0,2,0,0,2)(0,2,0,1,0)(0,2,0,1,2)(0,2,0,2,0)(0,2,0,2,1)(0,2,1,0,0)(0,2,1,0,1)(0,2,1,0,2)(0,2,1,1,0)(0,2,1,1,2)(0,2,1,2,0)(0,2,1,2,1)(0,2,2,0,0)(0,2,2,0,1)(0,2,2,0,2)(0,2,2,1,0)(0,2,2,1,1)(0,2,2,2,0)(0,2,2,2,2)(1,0,0,0,0)(1,0,0,0,1)(1,0,0,0,2)(1,0,0,1,0)(1,0,0,1,2)(1,0,0,2,0)(1,0,0,2,1)(1,0,1,0,0)(1,0,1,0,1)(1,0,1,0,2)(1,0,1,1,0)(1,0,1,1,2)(1,0,1,2,0)(1,0,1,2,1)(1,0,2,0,0)(1,0,2,0,1)(1,0,2,0,2)(1,0,2,1,0)(1,0,2,1,1)(1,0,2,2,0)(1,0,2,2,2)(1,1,0,0,0)(1,1,0,0,1)(1,1,0,0,2)(1,1,0,1,0)(1,1,0,2,0)(1,1,1,0,0)(1,1,1,0,1)(1,1,1,0,2)(1,1,1,1,0)(1,1,1,2,0)(1,1,2,0,0)(1,1,2,0,1)(1,1,2,0,2)(1,1,2,1,0)(1,1,2,2,0)(1,2,0,0,0)(1,2,0,0,1)(1,2,0,0,2)(1,2,0,1,0)(1,2,0,2,0)(1,2,1,0,0)(1,2,1,0,1)(1,2,1,0,2)(1,2,1,1,0)(1,2,1,2,0)(1,2,2,0,0)(1,2,2,0,1)(1,2,2,0,2)(1,2,2,1,0)(1,2,2,2,0)(2,0,0,0,0)(2,0,0,0,1)(2,0,0,0,2)(2,0,0,1,0)(2,0,0,1,1)(2,0,0,2,0)(2,0,0,2,2)(2,0,1,0,0)(2,0,1,0,1)(2,0,1,0,2)(2,0,1,1,0)(2,0,1,1,1)(2,0,1,2,0)(2,0,1,2,2)(2,0,2,0,0)(2,0,2,0,1)(2,0,2,0,2)(2,0,2,1,0)(2,0,2,1,2)(2,0,2,2,0)(2,0,2,2,1)(2,1,0,0,0)(2,1,0,0,1)(2,1,0,0,2)(2,1,0,1,0)(2,1,0,2,0)(2,1,1,0,0)(2,1,1,0,1)(2,1,1,0,2)(2,1,1,1,0)(2,1,1,2,0)(2,1,2,0,0)(2,1,2,0,1)(2,1,2,0,2)(2,1,2,1,0)(2,1,2,2,0)(2,2,0,0,0)(2,2,0,0,1)(2,2,0,0,2)(2,2,0,1,0)(2,2,0,2,0)(2,2,1,0,0)(2,2,1,0,1)(2,2,1,0,2)(2,2,1,1,0)(2,2,1,2,0)(2,2,2,0,0)(2,2,2,0,1)(2,2,2,0,2)(2,2,2,1,0)(2,2,2,2,0)->P3 ; (0,0,0,0,0)->P4
S2 (Consistant) : p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S3 (Consistant) : ~p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S4 (Consistant) : T ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S5 (Consistant) : ~c ; ~~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
S6 (Consistant) : c ; ~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->P3
*
* Tableau 
**********

S1 (Consistant) : ~<<1,3>>X~c ; ~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c ; ~<<1,3>>X~c/\~<<2,3>>X~~c/\<<1,2,3,4,5>>X(p\/~p) ; <<1,2,3,4,5>>X(p\/~p)
   Succ: (0,0,0,0,0)->S2 ; (0,0,0,0,0)->S3 ; (0,0,0,0,1)(0,0,0,0,2)(0,0,0,1,0)(0,0,0,1,1)(0,0,0,1,2)(0,0,0,2,0)(0,0,0,2,1)(0,0,0,2,2)(0,0,1,0,0)(0,0,1,0,1)(0,0,1,0,2)(0,0,1,1,0)(0,0,1,1,1)(0,0,1,1,2)(0,0,1,2,0)(0,0,1,2,1)(0,0,1,2,2)(0,0,2,0,0)(0,0,2,0,1)(0,0,2,0,2)(0,0,2,1,0)(0,0,2,1,1)(0,0,2,1,2)(0,0,2,2,0)(0,0,2,2,1)(0,0,2,2,2)(0,1,0,0,0)(0,1,0,0,1)(0,1,0,0,2)(0,1,0,1,0)(0,1,0,1,1)(0,1,0,2,0)(0,1,0,2,2)(0,1,1,0,0)(0,1,1,0,1)(0,1,1,0,2)(0,1,1,1,0)(0,1,1,1,1)(0,1,1,2,0)(0,1,1,2,2)(0,1,2,0,0)(0,1,2,0,1)(0,1,2,0,2)(0,1,2,1,0)(0,1,2,1,2)(0,1,2,2,0)(0,1,2,2,1)(0,2,0,0,0)(0,2,0,0,1)(0,2,0,0,2)(0,2,0,1,0)(0,2,0,1,2)(0,2,0,2,0)(0,2,0,2,1)(0,2,1,0,0)(0,2,1,0,1)(0,2,1,0,2)(0,2,1,1,0)(0,2,1,1,2)(0,2,1,2,0)(0,2,1,2,1)(0,2,2,0,0)(0,2,2,0,1)(0,2,2,0,2)(0,2,2,1,0)(0,2,2,1,1)(0,2,2,2,0)(0,2,2,2,2)(1,0,0,0,0)(1,0,0,0,1)(1,0,0,0,2)(1,0,0,1,0)(1,0,0,1,2)(1,0,0,2,0)(1,0,0,2,1)(1,0,1,0,0)(1,0,1,0,1)(1,0,1,0,2)(1,0,1,1,0)(1,0,1,1,2)(1,0,1,2,0)(1,0,1,2,1)(1,0,2,0,0)(1,0,2,0,1)(1,0,2,0,2)(1,0,2,1,0)(1,0,2,1,1)(1,0,2,2,0)(1,0,2,2,2)(1,1,0,0,0)(1,1,0,0,1)(1,1,0,0,2)(1,1,0,1,0)(1,1,0,2,0)(1,1,1,0,0)(1,1,1,0,1)(1,1,1,0,2)(1,1,1,1,0)(1,1,1,2,0)(1,1,2,0,0)(1,1,2,0,1)(1,1,2,0,2)(1,1,2,1,0)(1,1,2,2,0)(1,2,0,0,0)(1,2,0,0,1)(1,2,0,0,2)(1,2,0,1,0)(1,2,0,2,0)(1,2,1,0,0)(1,2,1,0,1)(1,2,1,0,2)(1,2,1,1,0)(1,2,1,2,0)(1,2,2,0,0)(1,2,2,0,1)(1,2,2,0,2)(1,2,2,1,0)(1,2,2,2,0)(2,0,0,0,0)(2,0,0,0,1)(2,0,0,0,2)(2,0,0,1,0)(2,0,0,1,1)(2,0,0,2,0)(2,0,0,2,2)(2,0,1,0,0)(2,0,1,0,1)(2,0,1,0,2)(2,0,1,1,0)(2,0,1,1,1)(2,0,1,2,0)(2,0,1,2,2)(2,0,2,0,0)(2,0,2,0,1)(2,0,2,0,2)(2,0,2,1,0)(2,0,2,1,2)(2,0,2,2,0)(2,0,2,2,1)(2,1,0,0,0)(2,1,0,0,1)(2,1,0,0,2)(2,1,0,1,0)(2,1,0,2,0)(2,1,1,0,0)(2,1,1,0,1)(2,1,1,0,2)(2,1,1,1,0)(2,1,1,2,0)(2,1,2,0,0)(2,1,2,0,1)(2,1,2,0,2)(2,1,2,1,0)(2,1,2,2,0)(2,2,0,0,0)(2,2,0,0,1)(2,2,0,0,2)(2,2,0,1,0)(2,2,0,2,0)(2,2,1,0,0)(2,2,1,0,1)(2,2,1,0,2)(2,2,1,1,0)(2,2,1,2,0)(2,2,2,0,0)(2,2,2,0,1)(2,2,2,0,2)(2,2,2,1,0)(2,2,2,2,0)->S4 ; (1,0,0,1,1)(1,0,0,2,2)(1,0,1,1,1)(1,0,1,2,2)(1,0,2,1,2)(1,0,2,2,1)(1,1,0,1,1)(1,1,0,2,2)(1,1,1,1,1)(1,1,1,2,2)(1,1,2,1,2)(1,1,2,2,1)(1,2,0,1,2)(1,2,0,2,1)(1,2,1,1,2)(1,2,1,2,1)(1,2,2,1,1)(1,2,2,2,2)(2,0,0,1,2)(2,0,0,2,1)(2,0,1,1,2)(2,0,1,2,1)(2,0,2,1,1)(2,0,2,2,2)(2,1,0,1,2)(2,1,0,2,1)(2,1,1,1,2)(2,1,1,2,1)(2,1,2,1,1)(2,1,2,2,2)(2,2,0,1,1)(2,2,0,2,2)(2,2,1,1,1)(2,2,1,2,2)(2,2,2,1,2)(2,2,2,2,1)->S5 ; (0,1,0,1,2)(0,1,0,2,1)(0,1,1,1,2)(0,1,1,2,1)(0,1,2,1,1)(0,1,2,2,2)(0,2,0,1,1)(0,2,0,2,2)(0,2,1,1,1)(0,2,1,2,2)(0,2,2,1,2)(0,2,2,2,1)(1,1,0,1,2)(1,1,0,2,1)(1,1,1,1,2)(1,1,1,2,1)(1,1,2,1,1)(1,1,2,2,2)(1,2,0,1,1)(1,2,0,2,2)(1,2,1,1,1)(1,2,1,2,2)(1,2,2,1,2)(1,2,2,2,1)(2,1,0,1,1)(2,1,0,2,2)(2,1,1,1,1)(2,1,1,2,2)(2,1,2,1,2)(2,1,2,2,1)(2,2,0,1,2)(2,2,0,2,1)(2,2,1,1,2)(2,2,1,2,1)(2,2,2,1,1)(2,2,2,2,2)->S6
S2 (Consistant) : p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S3 (Consistant) : ~p ; p\/~p ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S4 (Consistant) : T ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S5 (Consistant) : ~c ; ~~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4
S6 (Consistant) : c ; ~~c ; <<1,2,3,4,5>>XT
   Succ: (0,0,0,0,0)->S4

#2 Updated by Thorsten Wißmann over 3 years ago

The published version of cool from january also tells "unsatisfiable". So it's a bug being there since the beginning of the CL implementation in cool.

#3 Updated by Thorsten Wißmann over 3 years ago

  • Subject changed from Strange CL result to Wrong CL result

#4 Updated by Thorsten Wißmann over 3 years ago

  • Status changed from In Progress to Closed

Fixed by η-conversion via 6e618918d31464ad719c8cc00ec429d4e9fd719d.

Also available in: Atom PDF