Bug #13

Wrong CL result

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
```

Bug #14: Strange CL resultClosed

History

#1 Updated by Thorsten Wißmannover 4 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ßmannover 4 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ßmannover 4 years ago

• Subject changed from Strange CL result to Wrong CL result

#4 Updated by Thorsten Wißmannover 4 years ago

• Status changed from In Progress to Closed