imported>Pascal: /* Category */

2009-11-20T17:01:27Z

imported>Nicolas: New page: A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour (new antecedent, a different WD predicate, ...), even after the old imp...

2009-10-06T17:55:41Z

New page: A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour (new antecedent, a different WD predicate, ...), even after the old imp...

New page

A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour (new antecedent, a different WD predicate, ...), even after the old implementation was used to prove models. This entails potential problems: what happens if we try to reuse/replay a proof rule serialized by the old reasoner implementation ? There might be unexpected failures, or even worse: silent false successes. Thus, we have to be aware of reasoner implementation changes. This is achieved through a reasoner versioning mechanism.

== A new published interface ==

The {{class|IVersionedReasoner}} interface extends the existing {{class|IReasoner}} interface and provides a method to get the reasoner version ({{method|getVersion()}}), which is defined as a non-negative integer.

To maintain backward compatibility with existing, potentially externally contributed, reasoners, it is not possible to impose the new interface to all reasoners. There will then exist versioned and non-versioned reasoners, all working together.

== Version serialization ==

To be efficient, the version must also be stored in proof rules, so that it can be checked when trying to reuse them. Rather than adding yet another xml attribute into proof files, it has been decided to concatenate the version to the reasoner name, using the following syntax:

reasonerName:version

When reusing a proof, version conflicts between serialized version and currently registered reasoner version are detected and processed, by trying to apply the latest one.

== Example ==

The following is an example implementation of the new {{class|IVersionedReasoner}} interface:

<pre>
public class Example implements IVersionedReasoner {

private static final String REASONER_ID = PLUGIN_ID + ".example";
private static final int VERSION = 15;

public void serializeInput(IReasonerInput input, IReasonerInputWriter writer)
throws SerializeException {
// as usual
}

public IReasonerInput deserializeInput(IReasonerInputReader reader)
throws SerializeException {
// as usual
}

public IReasonerOutput apply(IProverSequent seq, IReasonerInput input,
IProofMonitor pm) {
// as usual
}

public String getReasonerID() {
return REASONER_ID;
}

public int getVersion() {
return VERSION;
}

}
</pre>

← Older revision		Revision as of 17:01, 20 November 2009
Line 50:		Line 50:
	}		}
	</pre>		</pre>

			[[Category: Developer documentation]]

Versioned Reasoners - Revision history

imported>Pascal: /* Category */

imported>Nicolas: New page: A reasoner implementation is not necessarily frozen code. It may evolve in time, to fix bugs or modify the behaviour (new antecedent, a different WD predicate, ...), even after the old imp...