testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
testTautology44: unknown term operator: isSet(*)
Clover Coverage Report
Coverage timestamp: Fri May 24 2013 13:47:27 UTC
../../../../../../img/srcFileCovDistChart9.png 45% of files have more coverage
12   112   8   2.4
4   36   0.67   5
5     1.6  
1    
 
  CalculateTruth       Line # 28 12 8 85.7% 0.85714287
 
  (145)
 
1    /* This file is part of the project "Hilbert II" - http://www.qedeq.org
2    *
3    * Copyright 2000-2013, Michael Meyling <mime@qedeq.org>.
4    *
5    * "Hilbert II" is free software; you can redistribute
6    * it and/or modify it under the terms of the GNU General Public
7    * License as published by the Free Software Foundation; either
8    * version 2 of the License, or (at your option) any later version.
9    *
10    * This program is distributed in the hope that it will be useful,
11    * but WITHOUT ANY WARRANTY; without even the implied warranty of
12    * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13    * GNU General Public License for more details.
14    */
15   
16    package org.qedeq.kernel.bo.logic.model;
17   
18    import org.qedeq.kernel.se.base.list.Element;
19    import org.qedeq.kernel.se.common.DefaultModuleAddress;
20    import org.qedeq.kernel.se.common.ModuleContext;
21   
22   
23    /**
24    * This class calculates a new truth value for a given formula for a given interpretation.
25    *
26    * @author Michael Meyling
27    */
 
28    public final class CalculateTruth {
29   
30    /** Interpretation for variables. */
31    private final Interpreter interpreter;
32   
33    /**
34    * Constructor.
35    *
36    * @param model Model we use for testing.
37    */
 
38  349 toggle private CalculateTruth(final Model model) {
39  349 interpreter = new Interpreter(model);
40    }
41   
42    /**
43    * Test if given formula is a tautology. This is done by checking a default model and
44    * iterating through variable values.
45    *
46    * @param formula Formula.
47    * @return Is this formula a tautology according to our tests.
48    * @throws HeuristicException Evaluation failed.
49    */
 
50  0 toggle public static boolean isTautology(final Element formula)
51    throws HeuristicException {
52  0 final CalculateTruth calculator = new CalculateTruth(new SixDynamicModel());
53  0 return calculator.calculateTautology(new ModuleContext(new DefaultModuleAddress()),
54    formula);
55    }
56   
57    /**
58    * Test if given formula is a tautology. This is done by checking a model and
59    * iterating through variable values.
60    *
61    * @param model Model we use for testing.
62    * @param formula Formula.
63    * @return Is this formula a tautology according to our tests.
64    * @throws HeuristicException Evaluation failed.
65    */
 
66  141 toggle public static boolean isTautology(final Model model, final Element formula) throws HeuristicException {
67  141 final CalculateTruth calculator = new CalculateTruth(model);
68  141 Test failure here return calculator.calculateTautology(new ModuleContext(new DefaultModuleAddress()),
69    formula);
70    }
71   
72    /**
73    * Test if given formula is a tautology. This is done by checking a model and
74    * iterating through variable values.
75    *
76    * @param moduleContext Here we are within a module.
77    * @param model Model we use for testing.
78    * @param formula Formula.
79    * @return Is this formula a tautology according to our tests.
80    * @throws HeuristicException Evaluation failed.
81    */
 
82  208 toggle public static boolean isTautology(final ModuleContext moduleContext, final Model model,
83    final Element formula) throws HeuristicException {
84  208 final CalculateTruth calculator = new CalculateTruth(model);
85  208 return calculator.calculateTautology(moduleContext, formula);
86    }
87   
88    /**
89    * Test if given formula is a tautology. This is done by checking a model and
90    * iterating through variable values.
91    *
92    * @param moduleContext Here we are within a module.
93    * @param formula Formula.
94    * @return Is this formula a tautology according to our tests.
95    * @throws HeuristicException Evaluation failed.
96    */
 
97  349 toggle private boolean calculateTautology(final ModuleContext moduleContext, final Element formula)
98    throws HeuristicException {
99  349 boolean result = true;
100  349 do {
101  5950 Test failure here result &= interpreter.calculateValue(moduleContext, formula);
102    // System.out.println(interpreter.toString());
103  5920 } while (result && interpreter.next());
104  319 if (!result) {
105    // System.out.println(interpreter);
106    }
107    // System.out.println("interpretation finished - and result is = " + result);
108  319 return result;
109    }
110   
111   
112    }