Printing method(s) for ML_CM_1

[mbuit82]

I'm not sure if the conclusion's printout in this example is as intended—it is meant to show that A is not necessary? In any case it seems like \vee's printing method is skipped. Just thought I'd bring this up in case this is a bug!

Looking at it more carefully, the premise repeats every world twice for a total of 6 printouts with 3 worlds. I think something may be up with these printing methods.

EXAMPLE ML_CM_1: there is a countermodel.

Atomic States: 3

Semantic Theory: Brast-McKie

Premise:
1. \Box (A \vee B)

Conclusion:
2. \Box A \vee \Box B

Z3 Run Time: 0.0062 seconds

========================================

State Space:
  #b000 = □
  #b001 = a (world)
  #b010 = b (world)
  #b100 = c (world)

The evaluation world is: c

INTERPRETED PREMISE:

1.  |\Box (A \vee B)| = < {□}, ∅ >  (True in c)
      |(A \vee B)| = < {a, b, c}, ∅ >  (True in a)
        |A| = < {a}, {b, c} >  (True in a)
        |B| = < {b, c}, {a} >  (False in a)
      |(A \vee B)| = < {a, b, c}, ∅ >  (True in a)
        |A| = < {a}, {b, c} >  (True in a)
        |B| = < {b, c}, {a} >  (False in a)
      |(A \vee B)| = < {a, b, c}, ∅ >  (True in b)
        |A| = < {a}, {b, c} >  (False in b)
        |B| = < {b, c}, {a} >  (True in b)
      |(A \vee B)| = < {a, b, c}, ∅ >  (True in b)
        |A| = < {a}, {b, c} >  (False in b)
        |B| = < {b, c}, {a} >  (True in b)
      |(A \vee B)| = < {a, b, c}, ∅ >  (True in c)
        |A| = < {a}, {b, c} >  (False in c)
        |B| = < {b, c}, {a} >  (True in c)
      |(A \vee B)| = < {a, b, c}, ∅ >  (True in c)
        |A| = < {a}, {b, c} >  (False in c)
        |B| = < {b, c}, {a} >  (True in c)

INTERPRETED CONCLUSION:

2.  |\Box A \vee \Box B| = < ∅, {□} >  (False in c)
      |A| = < {a}, {b, c} >  (True in a)
      |A| = < {a}, {b, c} >  (False in b)
      |A| = < {a}, {b, c} >  (False in c)

Total Run Time: 0.1287 seconds

[benbrastmckie]

Yes, that is a bug which I fixed at some point (I'm not sure in which version). Here is the output I'm getting:

EXAMPLE MD_CM_1: there is a countermodel.

Atomic States: 1

Semantic Theory: Brast-McKie

Premise:
1. \Box (A \vee B)

Conclusions:
2. \Box A
3. \Box B

Z3 Run Time: 0.008 seconds

========================================

World Histories:
  W_0: (0:a)
  W_1: (0:b)

Evaluation Point:
  World History W_0: a
  Time: 0
  World State: a

INTERPRETED PREMISE:

1.  |\Box (A \vee B)| = < {a, b}, ∅ >  (True in W_0 at time 0)
      |(A \vee B)| = < {a, b}, ∅ >  (True in W_0 at time 0)
        |A| = < {a}, {b} >  (True in W_0 at time 0)
        |B| = < {b}, {a} >  (False in W_0 at time 0)
      |(A \vee B)| = < {a, b}, ∅ >  (True in W_1 at time 0)
        |A| = < {a}, {b} >  (False in W_1 at time 0)
        |B| = < {b}, {a} >  (True in W_1 at time 0)

INTERPRETED CONCLUSIONS:

2.  |\Box A| = < ∅, {a, b} >  (False in W_0 at time 0)
      |A| = < {a}, {b} >  (True in W_0 at time 0)
      |A| = < {a}, {b} >  (False in W_1 at time 0)

3.  |\Box B| = < ∅, {a, b} >  (False in W_0 at time 0)
      |B| = < {b}, {a} >  (False in W_0 at time 0)
      |B| = < {b}, {a} >  (True in W_1 at time 0)

Total Run Time: 0.0216 seconds

I'm on v.0.9.4. I'll try to announce any major releases.