LogicalSubDB.java

Go to the documentation of this file.

/*
 * (c) copyright 2008, Technische Universitaet Graz and Technische Universitaet Wien
 *
 * This file is part of jdiagengine.
 *
 * jdiagengine is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * jdiagengine is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * You should have received a copy of the GNU General Public License
 * along with jdiagengine. If not, see <http://www.gnu.org/licenses/>.
 *
 * Authors: Joerg Weber, Franz Wotawa
 * Contact: jweber@ist.tugraz.at (preferred), or fwotawa@ist.tugraz.at
 *
 */


package ATPInterface;

import java.util.*;

import theoremprover.*;
import hittingsetalg.*;


public class LogicalSubDB {

    // The unique name, e.g. "SD", "OBS", or "SDD".
    protected String name;

    // A container for the rules.
    protected LSentence rules;

    // The number of the rules.
    protected int numRules;

    // A parser for rules.
    protected LogicParser parser;

    // The assumption-based theorem-prover.
    protected ABTheoremProver theoremProver;

    public LogicalSubDB(String name) {
        this.name = name;
        rules = new LSentence();
        numRules = 0;
        parser = new LogicParser();
    }


    public String getName() {
        return name;
    }


    public void addRules(ArrayList newRules) throws LogicParseException {
        for (int i = 0; i < newRules.size(); ++i) {
  
            String ruleStr = (String)newRules.get(i);

            if (parser.parse(ruleStr)) {
                rules.addRules((LSentence)parser.result());
                ++numRules;
            } else {
                throw new LogicParseException(i + 1);
            }
        }
    }

    public int getNumRules() {
        return numRules;
    }

    public ArrayList getRulesAsStrings() {
        ArrayList result = new ArrayList();

        Iterator it = rules.rules.iterator();
        while(it.hasNext()) {
            result.add(it.next().toString());
        }

        return result;
    }

    public LSentence getRulesAsLSentence() {
        return rules;
    }

    public void clear() {
        rules = new LSentence();
        numRules = 0;
    }


    public void append(LogicalSubDB source) {
        rules.addRules(source.rules);
        numRules += source.numRules;
    }

    public boolean checkConsistency(boolean useFaultModes, String assumptionAB, 
                                    String assumptionNAB) throws LogicParseException {
         
        theoremProver = new ABTheoremProver();
         theoremProver = rules.asABPropositionalSentence(theoremProver);
         if (theoremProver == null) {
             throw new LogicParseException();
         }
         
         if (useFaultModes) {
             ArrayList posAssPrefixes = new ArrayList();
             posAssPrefixes.add(assumptionNAB);
             return (theoremProver.checkConsistency(posAssPrefixes));  
         } else {
             return (theoremProver.checkConsistency());         
         }
    }

    public ArrayList computeMinDiag(int maxExplSize, int maxNumExpl,
                                    boolean useFaultModes,  String assumptionAB, 
                                    String assumptionNAB, boolean verboseOutput) 

        throws IllegalAssumption {

        assert(theoremProver != null);
        
        ArrayList minHS;
        ArrayList result = new ArrayList();
        
        if (useFaultModes) {
            System.out.println("maxExplSize: " + maxExplSize);
            System.out.println("maxNumExpl: " + maxNumExpl);
            System.out.println("ass AB: " + assumptionAB);
            System.out.println("# assumptions: " + theoremProver.getAssumptions().size());
            System.out.println("# rules (altogher): " + rules.rules.size());
            if (verboseOutput) {
                System.out.println("--- rules: --- \n" + rules.toString());
            }
            MinHittingSetsFM hs = new MinHittingSetsFM(false, theoremProver, assumptionAB, assumptionNAB);
            
            hs.compute(maxExplSize, maxNumExpl); 
            minHS = hs.getMinHS();
            System.out.println("#minimal diagnoses: " + minHS.size());

        } else {
            MinHittingSets hs = new MinHittingSets(false, theoremProver);
            hs.compute(maxExplSize, maxNumExpl);
            minHS = hs.getMinHS();
        }
 
        Iterator itMinHS = minHS.iterator();
        while(itMinHS.hasNext()) {
            ArrayList explanation = new ArrayList();

            ArrayList candidate = (ArrayList)itMinHS.next();
            Iterator itCand = candidate.iterator();
            while(itCand.hasNext()) {
                Assumption a = (Assumption)itCand.next();
                explanation.add(a.toString());
            }

            result.add(explanation);
        }
        
        return result;
    }
}