/**
 *
 */
package edu.kit.iti.formal.pse.worthwhile.prover;

import java.util.Map;

import edu.kit.iti.formal.pse.worthwhile.interpreter.Value;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Expression;
import edu.kit.iti.formal.pse.worthwhile.model.ast.Program;

/**
 *
 */
public class SpecificationChecker {
    /**
	 *
	 */
    private Integer timeout = 0;

    /**
     * @return the timeout
     */
    public Integer getTimeout() {
	// begin-user-code
	return this.timeout;
	// end-user-code
    }

    /**
     * @param timeout
     *            the timeout to set
     */
    public void setTimeout(Integer timeout) {
	// begin-user-code
	this.timeout = timeout;
	// end-user-code
    }

    /**
	 *
	 */
    private ProverCaller prover;

    /**
     * @return the prover
     */
    public ProverCaller getProver() {
	// begin-user-code
	return this.prover;
	// end-user-code
    }

    /**
     * @param prover
     *            the prover to set
     */
    public void setProver(ProverCaller prover) {
	// begin-user-code
	this.prover = prover;
	// end-user-code
    }

    /**
	 *
	 */
    private FormulaGenerator transformer;

    /**
     * @return the transformer
     */
    public FormulaGenerator getTransformer() {
	// begin-user-code
	return this.transformer;
	// end-user-code
    }

    /**
     * @param transformer
     *            the transformer to set
     */
    public void setTransformer(FormulaGenerator transformer) {
	// begin-user-code
	this.transformer = transformer;
	// end-user-code
    }

    /**
	 *
	 */
    private ProverResult checkResult;

    /**
     * @return the checkResult
     */
    public ProverResult getCheckResult() {
	// begin-user-code
	return this.checkResult;
	// end-user-code
    }

    /**
     * @param checkResult
     *            the checkResult to set
     */
    public void setCheckResult(ProverResult checkResult) {
	// begin-user-code
	this.checkResult = checkResult;
	// end-user-code
    }

    /**
	 *
	 */
    public SpecificationChecker() {
	// begin-user-code
	// TODO Auto-generated constructor stub
	// end-user-code
    }

    /**
     * @param transformer
     */
    public SpecificationChecker(FormulaGenerator transformer) {
	// begin-user-code
	// TODO Auto-generated constructor stub
	// end-user-code
    }

    /**
     * @param formula
     * @param environment
     * @return
     */
    public Validity checkFormula(Expression formula, Map<String, Value> environment) {
	// begin-user-code
	// TODO Auto-generated method stub
	return null;
	// end-user-code
    }

    /**
     * @param program
     * @return
     */
    public Validity checkProgram(Program program) {
	// begin-user-code
	// TODO Auto-generated method stub
	return null;
	// end-user-code
    }
}
@@ -1,19 +1,8 @@
-/**%0A *%0A */%0A
 package 
@@ -257,16 +257,61 @@
 %0A%0A/**%0A *
+ Facade class for the %7B@link prover%7D package.
 %0A */%0Apub
@@ -343,37 +343,102 @@
 ecker %7B%0A    /**%0A
-%09 *%0A%09
+     * Time delta in seconds after which a prover call times out.%0A    
  */%0A    private 
@@ -794,37 +794,128 @@
 %0A    %7D%0A%0A    /**%0A
-%09 *%0A%09
+     * The %7B@link ProverCaller%7D that is called for checking the satisfiability of formulae.%0A    
  */%0A    private 
@@ -1272,37 +1272,136 @@
 %0A    %7D%0A%0A    /**%0A
-%09 *%0A%09
+     * The %7B@link FormulaGenerator%7D that is called for generating a formula from a %7B@link Program%7D.%0A    
  */%0A    private 
@@ -1820,37 +1820,90 @@
 %0A    %7D%0A%0A    /**%0A
-%09 *%0A%09
+     * The result of the last call to %7B@link prover%7D.%0A    
  */%0A    private 
@@ -2322,13 +2322,67 @@
 /**%0A
-%09 *%0A%09
+     * Uses %7B@link WPStrategy%7D as %7B@link transformer%7D.%0A    
  */%0A
@@ -2529,32 +2529,105 @@
 ram transformer%0A
+     *            Is called to transform %7B@link Program%7Ds into formulae.%0A
      */%0A    publ
@@ -2809,41 +2809,232 @@
   * 
-@param environment%0A     * @return
+           the %7B@link Expression%7D to check%0A     * @param environment%0A     *            a list of variable values and axioms%0A     * @return the %7B@link Validity%7D of %3Ccode%3Eformula%3C/code%3E when %3Ccode%3Eenvironment%3C/code%3E is applied
 %0A   
@@ -3257,23 +3257,115 @@
 %0A     * 
-@return
+           the %7B@link Program%7D to check%0A     * @return the %7B@link Validity%7D of %3Ccode%3Eprogram%3C/code%3E
 %0A     */

Add javadoc to SpecificationChecker where missing