edu.hkust.afchecker.tool
Class Verifier

java.lang.Object
  edu.hkust.afchecker.tool.Verifier

public class Verifier
extends java.lang.Object

Author: Andrew
File history: Created on July 22, 2011. Last update on Oct. 13, 2012.
Description: Adaptation fault model checker. This checker can takes as input a state machine (see details), and detects five types of adaptation faults.

Constructor Summary

Verifier(StateMachine sm)
State machine is used to construct the model checker

Method Summary

void	setEnvironmentData(java.util.ArrayList<EnvironmentData> data) Users are expected to feed the environment data set into AFChecker before starting interactive verification mode
void	verify(boolean undeterminism, boolean deadPredicate, boolean adaptationRace, boolean unreachability, boolean interactiveMode) The entry method of AFChecker.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

Verifier

public Verifier(StateMachine sm)

State machine is used to construct the model checker

Parameters:

sm - state machine

Method Detail

verify

public void verify(boolean undeterminism,
                   boolean deadPredicate,
                   boolean adaptationRace,
                   boolean unreachability,
                   boolean interactiveMode)

The entry method of AFChecker.

Parameters:

undeterminism - whether to check undeterministic adaptation faults

deadPredicate - whether to check dead rule predicate faults and dead state faults

adaptationRace - whether to check adaptation race and cycle faults

unreachability - whether to check unreachable state faults

interactiveMode - whether AFChecker should work in the interactive mode

setEnvironmentData

public void setEnvironmentData(java.util.ArrayList<EnvironmentData> data)

Users are expected to feed the environment data set into AFChecker before starting interactive verification mode

Parameters:

data - a list of environment data