fmrisc.ProgramExplorer.Tasks

Interface ProofNavigatorTask

All Superinterfaces:

Task

All Known Subinterfaces:

ClassicalTask, StateTask

All Known Implementing Classes:

ClassicalTaskBase, CorrectnessTask, FormulaTask, InvariantTask, ProofNavigatorTaskBase, SpecTask, StateTaskBase, TerminationTask, TypeCheckingTask

public interface ProofNavigatorTask
extends Task

A task that is suitable for solving with the RISC ProofNavigator.

Nested Class Summary

Nested classes/interfaces inherited from interface fmrisc.ProgramExplorer.Tasks.Task

Task.Observer, Task.Status

Method Summary

Modifier and Type	Method and Description
ProofNavigatorProblem	proofNavigatorProblem() Translate task into a problem for the RISC ProofNavigator.
void	reset() Reset the task to its initial (new) state.

Methods inherited from interface fmrisc.ProgramExplorer.Tasks.Task

getDirectory, getEvidence, getInfo, getName, getParent, getPosition, getStatus, isFinal, isOptional, print, resume, resumeOnNew, setObserver, setParent, setStatus

Method Detail

proofNavigatorProblem

ProofNavigatorProblem proofNavigatorProblem()

Translate task into a problem for the RISC ProofNavigator.

Returns:

the translation.

reset

void reset()

Reset the task to its initial (new) state.