Interface | Description |
---|---|
ReuseCapableOracle<S,I,O> |
Required interface for the
ReuseOracle . |
Class | Description |
---|---|
ReuseCapableOracle.QueryResult<S,O> | |
ReuseOracle<S,I,O> |
The reuse oracle is a
MembershipOracle.MealyMembershipOracle that is able to
Cache queries: Each processed query will not be delegated again (instead
the answer will be retrieved from the ReuseTree )
Pump queries: If the ReuseTree is configured to know which
symbols are model invariant input symbols via
ReuseOracle.ReuseOracleBuilder.withInvariantInputs(Set) (like a read from a
database which does not change the SUL) or configured for failure output
symbols via ReuseOracle.ReuseOracleBuilder.withFailureOutputs(Set) (e.g. a roll
back mechanism exists for the invoked symbol) the oracle could ''pump'' those
symbols inside a query once seen. |
ReuseOracle.ReuseOracleBuilder<S,I,O> |
Exception | Description |
---|---|
ReuseException |
This exception will be thrown whenever some nondeterministic behavior
in the reuse tree is detected when inserting new queries.
|
Copyright © 2015. All rights reserved.