Project

General

Profile

Support #3423

NuSmv Tests TODOs

Added by Anonymous over 2 years ago. Updated 11 months ago.

Status:
Rejected
Priority:
Normal
Assignee:
-
Category:
-
Target version:
Start date:
05/29/2018
Due date:
% Done:

0%

Estimated time:

Description

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());
}

Related issues

Related to Bug #3414: AF3 JUnit TestsClosed05/18/2018

History

#1 Updated by Anonymous over 2 years ago

// TODO: get(0) not justified.

#2 Updated by Anonymous over 2 years ago

  • Related to Bug #3414: AF3 JUnit Tests added

#3 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.14 RC2 (Tested, Bug-free) to Backlog

#4 Updated by Johannes Eder over 1 year ago

  • Assignee changed from Anonymous to Johannes Eder

#5 Updated by Johannes Eder 11 months ago

  • Status changed from New to Rejected
  • Assignee deleted (Johannes Eder)

Rejected as verification is no longer part of AF3.

Also available in: Atom PDF