search

jogiet / MOLOSS

MOLOSS is a satisfiability solver for modal logics
GNU General Public License v3.0
4 stars 2 forks source link

Some issue in the model returned #4

Closed Mystelven closed 6 years ago

Mystelven commented 6 years ago

Hello,

I tested moloss on a formula and I detect a bug in the model returned.

bash$ ./test.intohylo --get-model
c (p100) & ((~ (p101)) & (((~ (p101)) | (p100)) & (((~ (p102)) | (p101)) & (((~ (p103)) | (p102)) & (((~ (p100)) | (((~ (p1)) | ([r1] ((~ (p100)) | (p1)))) & ((p1) | ([r1] ((~ (p100)) | (~ (p1))))))) & (((~ (p101)) | (((~ (p2)) | ([r1] ((~ (p101)) | (p2)))) & ((p2) | ([r1] ((~ (p101)) | (~ (p2))))))) & (((~ (p102)) | (((~ (p3)) | ([r1] ((~ (p102)) | (p3)))) & ((p3) | ([r1] ((~ (p102)) | (~ (p3))))))) & (((~ ((p100) & (~ (p101)))) | ((<r1> ((p101) & ((~ (p102)) & (p2)))) & (<r1> ((p101) & ((~ (p102)) & (~ (p2))))))) & (((~ ((p101) & (~ (p102)))) | ((<r1> ((p102) & ((~ (p103)) & (p3)))) & (<r1> ((p102) & ((~ (p103)) & (~ (p3))))))) & (([r1] (((~ (p101)) | (p100)) & (((~ (p102)) | (p101)) & (((~ (p103)) | (p102)) & (((~ (p100)) | (((~ (p1)) | ([r1] ((~ (p100)) | (p1)))) & ((p1) | ([r1] ((~ (p100)) | (~ (p1))))))) & (((~ (p101)) | (((~ (p2)) | ([r1] ((~ (p101)) | (p2)))) & ((p2) | ([r1] ((~ (p101)) | (~ (p2))))))) & (((~ (p102)) | (((~ (p3)) | ([r1] ((~ (p102)) | (p3)))) & ((p3) | ([r1] ((~ (p102)) | (~ (p3))))))) & (((~ ((p100) & (~ (p101)))) | ((<r1> ((p101) & ((~ (p102)) & (p2)))) & (<r1> ((p101) & ((~ (p102)) & (~ (p2))))))) & ((~ ((p101) & (~ (p102)))) | ((<r1> ((p102) & ((~ (p103)) & (p3)))) & (<r1> ((p102) & ((~ (p103)) & (~ (p3))))))))))))))) & ([r1] ([r1] (((~ (p101)) | (p100)) & (((~ (p102)) | (p101)) & (((~ (p103)) | (p102)) & (((~ (p100)) | (((~ (p1)) | ([r1] ((~ (p100)) | (p1)))) & ((p1) | ([r1] ((~ (p100)) | (~ (p1))))))) & (((~ (p101)) | (((~ (p2)) | ([r1] ((~ (p101)) | (p2)))) & ((p2) | ([r1] ((~ (p101)) | (~ (p2))))))) & (((~ (p102)) | (((~ (p3)) | ([r1] ((~ (p102)) | (p3)))) & ((p3) | ([r1] ((~ (p102)) | (~ (p3))))))) & (((~ ((p100) & (~ (p101)))) | ((<r1> ((p101) & ((~ (p102)) & (p2)))) & (<r1> ((p101) & ((~ (p102)) & (~ (p2))))))) & ((~ ((p101) & (~ (p102)))) | ((<r1> ((p102) & ((~ (p103)) & (p3)))) & (<r1> ((p102) & ((~ (p103)) & (~ (p3)))))))))))))))))))))))))) 

c oracle minisat
c #propositions #worlds #relations #edges
v 103 1 1 6
v 1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 -101 -102 -103 0
v 1 2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 -102 -103 0
v r1 w0 w1
v r1 w0 w2
v r1 w1 w4
v r1 w1 w5
v r1 w2 w3
v r1 w2 w6
s SATISFIABLE

In gives a model which looks correct for the valuation but some information are missing.

You indicate on the first line v 103 1 1 6 that we have 103 variables (which is true) but only 1 world. However, in your valuation you count already 2 and in the relation between the worlds you go until w6 so 7 worlds (which is the smallest value in fact). Moreover, your relations are good, it is suppose to give in output a binary tree and you have it.

Thus, I have no doubt that you have found the correct model, it is just no well displayed I think :).

jogiet commented 6 years ago

There was in fact a problem in the model display.

https://github.com/Meleagant/MOLOSS/commit/3d3fec8aab584c9ce7974d74af93327c2a4e821f solved this.

tofgarion commented 6 years ago

I was about to push the same changes, thanks Josselin! I am too slow (or too old now)...

Mystelven commented 6 years ago

Hello,

Just to informed you that it is indeed perfectly correct now :)

s SATISFIABLE
v 103 7 1 6
v 1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 -101 -102 -103 0
v 1 2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 -102 -103 0
v 1 -2 3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 -102 -103 0
v 1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 102 -103 0
v 1 2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 102 -103 0
v 1 2 3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 102 -103 0
v 1 -2 3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 100 101 102 -103 0
v -1 -2 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 -17 -18 -19 -20 -21 -22 -23 -24 -25 -26 -27 -28 -29 -30 -31 -32 -33 -34 -35 -36 -37 -38 -39 -40 -41 -42 -43 -44 -45 -46 -47 -48 -49 -50 -51 -52 -53 -54 -55 -56 -57 -58 -59 -60 -61 -62 -63 -64 -65 -66 -67 -68 -69 -70 -71 -72 -73 -74 -75 -76 -77 -78 -79 -80 -81 -82 -83 -84 -85 -86 -87 -88 -89 -90 -91 -92 -93 -94 -95 -96 -97 -98 -99 -100 -101 -102 -103 0
v r1 w0 w1
v r1 w0 w2
v r1 w1 w4
v r1 w1 w5
v r1 w2 w3
v r1 w2 w6

Has been checked with mdk-verifier and the Kripke structure is indeed a model of the formula :). I will keep you informed about the performance of Moloss ;) Cheers ! :)