jogiet / MOLOSS

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

Problem with the model v2 #5

Closed Mystelven closed 6 years ago

Mystelven commented 6 years ago

Hello,

I find another bug related to the model-output. Again does not seems to be something big, just a display problem. Here is the StackTrace:

c (p100) & ((~ (p101)) & ([r1] (((~ (p101)) | (p100)) & (((~ (p102)) | (p101)) & (((~ (p100)) | (((~ (p1)) | ([r1] ((~ (p100)) | (p1)))) & ((p1) | ([r1] ((~ (p100)) | (~ (p1))))))) & (((~ (p101)) | (((~ (p2)) | ([r1] ((~ (p101)) | (p2)))) & ((p2) | ([r1] ((~ (p101)) | (~ (p2))))))) & ((~ ((p100) & (~ (p101)))) | ((<r1> ((p101) & ((~ (p102)) & (p2)))) & (<r1> ((p101) & ((~ (p102)) & (~ (p2))))))))))))) 

c oracle minisat
c #propositions #worlds #relations #edges
s SATISFIABLE
v 101 1 1 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 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 0

There is 2 worlds displayed, and they are basically the same, except that in one, p100 is true, and in the other one p100 is false. In my opinion, it is missing the link r1 w0 w1 and it should be 2 worlds not one.

jogiet commented 6 years ago

Actually, the problem was already existing in the latest issue (8 wolds valuations were printed !) but https://github.com/Meleagant/MOLOSS/commit/2469c26a8ccabe2e6c5946a1ea07c6aebc353453 corrected it. Basically, it was a bound mistake in the for loop