NuSmv Tests TODOs
org.fortiss.af3.tools.nusmv.base.NuSMVTestBase
protected AG ag(String exp) {
// TODO (VA) The following null should be turned into a meaningful
value.
// Typically, the NuSMV file should be used and turned into a TypeScope.
return NuSMVModelFactory.ag(compiler.compileTerm(exp, null));
}
/ Creates a G. */
protected G g(String exp) {
// TODO (VA) The following null should be turned into a meaningful
value.
// Typically, the NuSMV file should be used and turned into a TypeScope.
return NuSMVModelFactory.g(compiler.compileTerm(exp, null));
}
/ Adds an init statement to the current module */
protected void init(LocalVariable lv, String initAsString) {
// TODO (VA) The following null should be turned into a meaningful
value.
// Typically, the NuSMV file should be used and turned into a TypeScope.
addInit(currentModule, lv, compiler.compileTerm(initAsString, null));
}
org.fortiss.af3.tools.nusmv.base.tests.PrimitiveTests
//TODO: refactor to have actual Primitive Tests and ‘more complex’
test
//TODO: test Bounded Modelchecking
org.fortiss.af3.tools.nusmv.base.tests.SmokeTest
public void simpleCounterexampleTest() {
newNuSMVFile(“simpleCounterexample”);
createTestModule();
RangeType tpe = NuSMVModelFactory.createRangeType(0, 100);
LocalVariable counter = newLocalVariable(“counter”, tpe);
init(counter, “1”);
// TODO
// next(counter, “counter < 15”, “counter + 1”);
// next(counter, “true”, “counter”);
ltlSpec(g(“counter < 5”));
NuSMVResult result = runNuSMV(LTL, g(“counter < 5”));
assertNotNull(result);
assertFalse(result.isSpecificationFulfilled());
assertSame(4, result.getCounterexampleStates().size());
CounterexampleState cs = result.getCounterexampleStates().get(0);
assertEquals(“1”, cs.getEntries().get(0).getValue());
}
(from redmine: issue id 3423, created on 2018-05-29, closed on 2019-12-10)
- Relations:
- relates #3414 (closed)