cyrille-artho / modbat Goto Github PK

The included dependencies on libraries for Scala 2.11 contain some instances of code that won't run on 2.12, e.g.

$ scala modbat.jar --classpath=modbat-test.jar modbat.test.ChooseTest
java.lang.NoSuchMethodError: scala.Predef$.refArrayOps([Ljava/lang/Object;)Lscala/collection/mutable/ArrayOps;
	at modbat.config.ConfigMgr.<init>(ConfigMgr.scala:73)
	at modbat.mbt.Main$.main(Main.scala:12)
	at modbat.mbt.Main.main(Main.scala)

Unfortunately, it seems that the only solution is to bump the libraries to 2.12 in build.gradle, which may or may not be backwards compatible. It doesn't seem like there's a way of letting Gradle Do The Right Thing automatically. sigh

Any test that tests the output of "-s" should remove terminal escape codes for bold and normal font:
ESC[0m
ESC[1m
At the moment, ConfigTest does not compare the output, so this is low priority until tests are actually affected by this.

The sources are currently all in src/scala. Gradle normally assumes src/[lang]/main and src/[lang]/test.

The main and test files should therefore be separated. There are also a few Java files. So I suggest the following:

1. Make directories src/java/main, src/java/test, src/scala/main, src/scala/test.
2. Move the files to the right place:

• Move Java files in src/scala/modbat/test to src/test/java/modbat/test (keeping the package name "test" for now).
• Move all other Java files in src/scala/modbat to src/main/java/modbat.
• Move all remaining files in src/scala/modbat/test to src/test/scala/modbat/test.
• Move all remaining files in src/scala/modbat to src/main/scala/modbat.

3. Also build the jar files in the usual location.

This is useful in particular to find issues with static fields that do not get reset when re-running run (from a test harness) instead of main as a process. The same issue may appear (much more likely/often) with Main.run in Modbat.

The new feature for path coverage should be automatically tested (issue #69) and documented.
The documentation should:

• mention this feature in the README,
• have more detailed information on the wiki,
• include a wiki entry page.

For this, we also need to create a simple wiki entry page, stating that most features are (currently) documented in the README but will be moved to the wiki over time (issue #44).

Tests perform differently when project is build with gradle.

Try the following:

• Changes in MBT

1. Class Timer in file MBT.scala:

  class Timer(val t: Long) extends Thread {
    override def run() {
      Log.fine(name + ": Started staying for " + t + " ms.")
      Thread.sleep(t)
      MBT.stayLock.synchronized {
        staying = false
        MBT.stayLock.notify()
      }
      Log.fine(name + ": Finished staying.")
    }
  }

Class Timer should be renamed to something fitting its new purpose, e.g., WakeUp.
The first two lines in run (logging, sleep) should be removed.

2. In executeTransition (same file):

          case Some((t1, t2)) => {
            MBT.stayLock.synchronized {
              staying = true
            }
            val stayTime = (if (t1 == t2) t1 else rng.choose(t1, t2)).asInstanceOf[Long]
            new Timer(stayTime).start()
          }

Remove the line that starts a new timer. Instead, the timer is registered as a task with the mock scheduler: schedule(0, stayTime, new WakeUp()). The wakeup task is not started here.

• Timer usage
  To keep the changes small, the mock scheduler fulfills the tasks that are currently handled by Timer.
  With the modified class (now WakeUp), the rest of the inter-thread communication is still the same.
  The use of the mock scheduler would allow us to use real time as well (with the "real" scheduler), without changing the code much.
  The changes for this are as follows:

1. Start the mock scheduler (either at the beginning of using Modbat, if no scheduler exists yet, or when stay is used for the first time).
2. In Modbat.scala: Change
   MBT.stayLock.wait()
   to code that advances the virtual time enough (using tick) to get at least one task ready; the WakeUp task will set staying to false, and allow the repeated invocation of allSuccessors to succeed.

The unit tests in src/test should reflect the package hierarchy in src/main. Currently, there are example models in src/test/scala/modbat/{test,examples}, but the unit tests that use them are in src/test/scala/modbat/mbt. They should be moved to the other two directories, and renamed if needed.

The warning appears due to backward compatibility with Scala 2.10, which is no longer needed.

For being able to use a unit-test framework on some system tests, failing configurations have to avoid exiting the VM. Therefore, it is essential that the use of System.exit is minimized.
This requires refactoring a lot of existing code:

• main cannot have a return value, so a different function (e.g., run) should provide the same functionality with a return value instead of exit code. main continues to provide an exit code for system tests and production usage, calling run internally.
• Any usage of System.exit should be rewritten such that, at the top level, run returns the status as an exit code, and only main actually exits.

As of now, there are 13 instances of System.exit in the code base.

Let's try to build the JAR file at the beginning of test.sh:

#!/bin/sh
CWD=`pwd`
cd build/classes/scala/test
jar cf build/modbat-examples.jar modbat/examples/
jar cf build/modbat-test.jar modbat/test
mv modbat-*.jar ../../..
cd ${CWD}

... # remaining script

There is already one test under scalatest, but the output is not checked. Before it can truly replace existing tests, we should have a way of using scalatest matchers to check the occurrence of certain elements in the log, such as should contain inOrder.
This should be implemented such that the stdout and stderr outputs are checked against the patterns.
Ideally, we could learn some common patterns through analysis of the test inputs, and the given test outputs.

After Rui's refactoring for path coverage, we will have an index counting the number of model instances for each type (class name). This eliminates the need for putting the counter into the name. Instead, a corresponding getter or toString function should return className + "-" + idx, and the extra field modelName should be removed.

The README should be updated to ensure:

• The commands to build Modbat are updated (using gradle).
• The commands to run Modbat include the fact that the jar files are in "build/" by default.
• The markdown syntax is used for titles etc.

The README file and the wiki should be updated with a description of these new features.

Currently, in the ScalaTest framework (issue #55), stderr and stdout are redirected to files. The name of these files consists of the name of the model class as the directory name, together with a long filename that consists of all the options (concatenated).
It is much easier in the long run if we use the name of the test case itself. This requires finding out if we can access this information from within the test.
We can do this at the end. For the main phase of the project, trying to synthesize a partial test oracle on the log output, it is much easier if we keep the filenames unchanged.

The warning appears due to backward compatibility with Scala 2.10, which is no longer needed.

APP="scala -cp build modbat.config.ConfigTest"

run 0 $APP
run 0 $APP -h
run 0 $APP -s

Relies on classes being in build/modbat/...
Gradle seperates them depending on subproject and language.

For unit testing, we need to override environment variable CLASSPATH.

To achieve this, use the code described under
"For use in scenarios where you need to set specific environment values for unit tests"
at https://stackoverflow.com/questions/318239/how-do-i-set-environment-variables-from-java

Use that and change System.setProperty to setEnv.
You also have to create a new Map "newEnv" with one entry that you pass to setEnv.

Once this works, the extra argument "--classpath=build/modbat-test.jar" can be removed in all (about 10) tests in src/test/scala:

• src/test/scala/modbat/mbt/ChooseTest.scala
• src/test/scala/modbat/mbt/InvokeTransitionTest.scala
• src/test/scala/modbat/mbt/SetWeightTest.scala
• src/test/scala/modbat/mbt/TimeTest.scala

Displaying path coverage is interactive to allow a user to select what parts of the coverage to display. This cannot be used with automated testing; the tests are currently disabled due to this.

We can use mock testing in case Modbat.isUnitTest is true.

See:
http://www.scalatest.org/user_guide/testing_with_mock_objects
https://scalamock.org/user-guide/advanced_topics/

The mock should replace readLine and return the right sequence of qs and other inputs.

Currently, stay allows a model to stay dormant for a while. The new code (issue #33) will integrate this functionality with an implementation that supports virtual time. This allows us to skip ahead to the next event, instead of waiting with Thread.sleep.
If we use this in a simulated environment, the environment also needs to be able to skip time. We therefore need to provide a custom sleep function in the model.
If virtual time is used, Model.sleep internally calls advance on the virtual timer instead of sleeping.
Later on, we can also support real time, where all calls to advance are replaced with Thread.sleep.

The feature to adjust the weight dynamically should be incorporated into this version of Modbat.
For this, we probably should also add getWeight, for unit testing.
Overall, we should have a couple of tests:

1. A unit test that creates a new transition and uses set/get to ensure that get returns the parameter given to set.
2. As above, but with set using a negative value; this should throw IllegalArgumentException.
3. A simple test model that uses setWeight to get a result (with a couple of tests) that is clearly different from the result with setWeight absent.
4. A test where all outgoing transitions have the same weight so setWeight does not change anything.

Probably it is not possible at this time to load a class directly from a unit test, only through the front-end of Modbat (Main.run).

Currently, Modbat has only a README as documentation. This file is becoming too long, so the contents should be split up into a wiki with multiple pages.
There are also many aspects of Modbat that are not fully documented, or not documented at all in the README; some aspects are documented only in research papers. It is time to pull all that information together and present it in a unified, accessible way.

The overall structure of the README is quite good, but it is far too long now. The README should be kept with information on installing and starting the tool, but any details should be moved to a wiki.

The envisioned structure of the wiki:

• Title
• Summary
• Installation
• An introduction to model-based testing in general: This is not in the README, but several research publications and presentations have this information. The task is to provide an abridged introduction about the concepts, with references to literature, and examples (as graphical models) that illustrate the concepts.
• Key syntax
• Basic usage; how to compile your own model
• How to read the error traces
• Link to the first Modbat tutorial. The tutorial should be merged with the main wiki; its documentation (README) should also be split into multiple steps, each on its own wiki page. Besides the problem, some hints to the solution should be given, so someone who uses this for self-study finds the material more accessible. Finally, a few more advanced examples should be included, to show other features.
• Semantics of the models
• Preconditions and assertions
• Inheritance
• Advanced features. Some of them are documented in the README, others in papers, others not yet at all.
• Exceptional outcomes should be defined conceptually and then syntactically, building on the definitions of the SEFM paper.
• API functions
• Observer models
• Helper method annotations
• Field annotations
• Visualization
• Replaying traces
• Other test configuration options
• Troubleshooting
• Contributing to Modbat: coding conventions, self-test framework

Related to #26 #29:
It is possible that the coverage is not reset by simply calling init, as the original code assumed Main.main would be run, and all coverage data would be empty.
With two tests using the same model, executing different transitions due to different initial states or different choices taken, we can ensure that the coverage information is actually reset.

When a child model is created inside the constructor of the parent, the sets of transitions of the models get mixed up. Example:

  class LaunchFail extends Model {
    val child = new LaunchFailChild()
    "parent-init" -> "parent-main" := {
      launch(child)
    }
    "parent-main" -> "parent-end" := {
    }
  }

This is a part of issue #55.
At the moment, some test cases have a truncated output.

1. The "diff" function in the should show that one stream is shorter than the other one.
   Current output:

SimpleCounter:
SimpleCounter1
it1 =        1 3ba471c1785a0175
it2 =        1 3ba471c1785a0175

Desired output (note: only mismatching lines, or the lines preceding a mismatch upon truncation, should be shown):

SimpleCounter:
SimpleCounter1
it1 =        1 3ba471c1785a0175
it2 =        1 3ba471c1785a0175
it1: end of file
it2 = 

(In this case, it2 has an empty line.)

2. (Only) for failing tests, the shutdown handler should be invoked explicitly. At the point where the exception is caught, the test harness should do the following:

  case e: Exception => {
    Modbat.ShutdownHandler.run
    ret=1
  }

Issue #33 now supports virtual time.
To use it, we first have to refactor the "smart house" model to use the new Model.sleep (after issue #40 is done). After that, we want to support both timing models:

1. Use a similar scheduler (perhaps the Akka scheduler?) to support real time using a similar interface.
2. Encapsulate the differences between real and virtual time in an adapter class.
3. Add a configuration option to choose between the two implementations at start-up.

See #54. Currently, we are about to convert some test cases as part of issue #55, including test cases with no CLASSPATH setting. setEnv needs to be adapted that it always clears the environment before setting specific settings; the map of such settings may also be empty.

Pass entire configuration object to MBT rather than individual parameters, as there are too many now.

For the configuration tests such as ConfigTest, we will need a ConfigurationTestHarness that is similar to ModbatTestHarness, except that (maybe) we don't need to specify which JAR file to use here, as it's probably always the same one. There are two cases, though:

1. ConfigTest is called directy
2. The test is run by loading an executable JAR file.

Ant includes classfiles from asm and config in the main jar. Including asm is convenient in order to have a runnable jar. config could either be on the classpath or included.

This function is currently too long and can be split into path coverage and other coverage, and otherwise refactored into multiple functions.

The few existing model tests (in src/test) currently set the classpath via the command line, because setting the environment variable did not work. This should be fixed as some point to avoid this redundancy.

This relates to #23, #26, and #27. Modbat has been written to be run as a main program, and to be run inside a unit test framework, several side effects have to be avoided.
One is that a shutdown handler should only be registered once. When run via the new Main.run, the shutdown handler is registered every time, resulting in an exception. This has to be fixed by checking first if a shutdown handler already exists, before registering it.

Observers (monitors) state machines are "passive" state machines that only advance when some preconditions are fulfilled. They are intended to be used to monitor a system, but not provide inputs to it.
This feature has been barely used so far, and it seems not to be included in path coverage, in exploreSuccessors:

            if (TransitionResult.isErr(observerResult)) {
              return (observerResult, result._2)
            }

This is the only code that returns without updating path coverage: storePathInfo(result, successor, backtracked, ... is otherwise everywhere before the function returns.
Perhaps this was an oversight; in any case, it is not tested. It is not high priority, and we could simply document that path coverage does not include observer state machines.
(For our work on state space search, this is actually better; the observers do not generate tests, and thus it is not useful to track their path.)

For performance and ease of use, we would like to run upcoming tests under scalatest.
To make sure we have a working test harness and an example, I would like to migrate Choose00, the simplest test that currently exists.

For this, we need to have a harness ModbatTestHarness, which is similar to ConfigTest, to run Main.main:

package modbat.mbt

import java.io.ByteArrayOutputStream
import java.io.FileDescriptor
import java.io.FileOutputStream
import java.io.PrintStream

import org.scalatest._

object ModbatTestHarness {
  def testMain(args: Array[String]): (Int, List[String], List[String]) = {
    val out: ByteArrayOutputStream = new ByteArrayOutputStream() 
    val err: ByteArrayOutputStream = new ByteArrayOutputStream()
    val ret = 0

    Console.withErr(err) {
      Console.withOut(out) {
        ret = Main.run(args)
      }
    }
    (ret, scala.io.Source.fromString(out.toString).getLines().toList, scala.io.Source.fromString(err.toString).getLines().toList)
  }
}

Another class should be used to test different features, e.g., ChooseTest. For now, we'll have only one test there, but we can migrate more tests in the future and add new tests:

class ChooseTest extends FlatSpec with Matchers {
  "Choose00" should "pass with one transition" in {
    val result = ConfigTest.testCtor(Array("-s=1", "-n=1", "--no-redirect-out", "modbat.test.Choose00"))
    result._1 should be(0)
    result._2 should contain ... // three checks, probably in three lines
    result._3 shouldBe empty
  }
}

In the output, there are three lines that are relevant. I'd like to check them against the actual content without the "preamble" [INFO], and without looking at the order of the output. So please add three checks, to verify that each substring occurs (e.g., "1 tests executed, 1 ok, 0 failed."):

[INFO] 1 tests executed, 1 ok, 0 failed.
[INFO] 2 states covered (100 % out of 2),
[INFO] 1 transitions covered (100 % out of 1).

We would like to use a unit test framework for most (all?) tests, to abolish our own test runner, and to allow parallel testing.
First, a proof of concept is needed that shows how two or three tests run inside such a framework and possibly interact because static fields are not reset.
This may in turn require changes in Modbat's configuration handling or even beyond.

SKIP = \0 should be SKIP = \u0000.

Presumably the parameter totalW can be eliminated in some places.

The tool should not try to load a model when there is none (and exit). This is probably a side effect of the refactoring of System.exit (issue #27).

• Make util/FieldUtil.scala part of config

Currently, tests checking the output of "-h", or other options that emit the version number, fail if the upcoming version is not tagged yet. Making the tests pass may require tagging, testing, and re-tagging.
It is undesirable that the test output has to be kept in sync with the tag and actual version.
After migrating to a unit test framework (#12), even for only some tests, we can replace the fixed test against a test that checks the syntax/format of the output, but not the content.

Divide it into smaller functions.

In modbat-test/src/main/scala/modbat/test/GenLabel3.scala, there are two methods with an @States annotation.
In some JDKs, they get processed in the order in which they were declared, but this is not guaranteed and indeed inconsistent between JDKs.
Fixing this will require an adaptation of this part of the code in src/main/scala/modbat/mbt/MBT.scala:

  def registerStateSelfTrans(model: Model, isChild: Boolean) {
    val methods = MBT.getMethods(model)
    for (m <- methods) {

The methods should be sorted first before they are processed. An alphabetical order, probably produced by toGenericString, will provide a unique, canonical order.

This will change the outputs of many test cases, which will have to be updated.

Version tags will use just the version from now on, so version 3.3 will be tagged "3.3".

As a first step towards #23, it would be good to refactor and extend the existing example test:

1. Parse the outputs to stdout, stderr, and return them as a pair of lists of lines (Line[String], Line[String]).
2. Use matchers to check the key information: the lines should be matched against some test-specific information. In this case, there were two lines specified in the constructor, which should be part of the resulting text. stderr should be empty.

The configuration management module (modbat.config.ConfigMgr) represents all configuration options as variables, which use trait modbat.config.Configuration. This makes it very easy to add new options and check the range of parameters at run time. However, for unit testing, this has the problem that overriding the default results in a persistent setting.

We need to be able to reset the configuration options (usually in modbat.mbt.Configuration) back to their defaults before each new test. This can be done by adding the ability to clone to trait modbat.config.Configuration.

We need

1. a clone method for trait modbat.config.Configuration;
2. for each type of value, a unit test that clones a test configuration, alters a value on the clone, and ensures that the original still has the correct original setting.

The choice of an array is probably from legacy code.

All the executions of the test cases can be converted from a list of command-line arguments to a list of strings and calls to testMain in ModbatTestHarness.

We still want to keep bin/test.sh for reference, but we also want a version that (1) does not execute any tests (similar to option -n) but (2) still checks all the outputs (which -n does not do).

First, we want to convert a couple of test cases that share similar settings, and then adapt a part of bin/test.sh as (for example) bin/diff.sh, to check the log/err outputs. Once that works, we will convert all 250+ tests.