/*
 * Copyright (c) 2012 Mateusz Parzonka, Eric Bodden
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 *
 * Contributors:
 * Mateusz Parzonka - initial API and implementation
 */
package prm4j.indexing;

import prm4j.api.BaseEvent;
import prm4j.api.MatchHandler;

public abstract class BaseMonitorState {

    private final int index;

    public BaseMonitorState(int index) {
	this.index = index;
    }

    public abstract BaseMonitorState getSuccessor(BaseEvent baseEvent);

    /**
     * Tests, if the current state is an accepting state.
     *
     * @return <code>true</code> if the current state is accepting
     */
    public abstract boolean isAccepting();

    public abstract MatchHandler getMatchHandler();

    /**
     * Tests, if all successor states are dead states. (A dead state is a non-accepting state, where all successors are
     * dead states. Because final state <i>may</i> be an accepting state, it is not always a dead state.)
     *
     * @return <code>true</code> if all successor states are dead states
     */
    public abstract boolean isFinal();

    public int getIndex() {
	return index;
    }

}
@@ -460,140 +460,669 @@
 r;%0A%0A
-public abstract class BaseMonitorState %7B%0A%0A    private final int index;%0A%0A    public BaseMonitorState(int index) %7B%0A%09this.index = index
+/**%0A * Models the internal state of a %7B@link StatefulMonitor%7D where the state space may be finite or infinite.%0A *%0A * @see  %7B@link BaseMonitor%7D%0A */%0Apublic abstract class BaseMonitorState %7B%0A%0A    /**%0A     * Unique index for finite state spaces.%0A     */%0A    private final int index;%0A%0A    /**%0A     * Creates a monitor state assuming a finite state space. The monitor will have an unique index.%0A     *%0A     * @param index%0A     */%0A    public BaseMonitorState(int index) %7B%0A%09this.index = index;%0A    %7D%0A%0A    /**%0A     * Creates a monitor state assuming an infinite state space. This monitor will not have an unique index.%0A     */%0A    public BaseMonitorState() %7B%0A%09index = -1
 ;%0A  
@@ -1440,24 +1440,257 @@
 Handler();%0A%0A
+    /**%0A     * @return %3Ccode%3Etrue%3C/code%3E if the state space is finite, of %3Ccode%3Efalse%3C/code%3E if there may exist an infinite%0A     *         number of possible states.%0A     */%0A    public boolean isFinite() %7B%0A%09return index %3E= 0;%0A    %7D%0A%0A
     /**%0A    
@@ -2035,24 +2035,248 @@
 isFinal();%0A%0A
+    /**%0A     * Returns the unique index of this state if the state space is finite. A valid index is a non-negative integer.%0A     *%0A     * @return the unique index of this state or -1 if the state space is infinite.%0A     */%0A
     public i

Add finite/infinite state space distinction to BaseMonitorState