BRE:IN - A Backend for Reasoning about Interaction Networks with Temporal Logic

Judah Goldfeder and Hillel Kugler

How to build and run NAE (BRE:IN):

Dependencies:
NAE requires both the java SDK and NuSMV to be on the path.  It was tested using java version 1.8.0_144 and NuSMV-2.6.0.

Building:
to build NAE type the following two commands from within the NetworkAnalysisEngine directory:
>javac NAE/*.java validate/*.java
>jar cvfm NAE.jar NAE/manifest.txt NAE/*.class validate/*.class

This creates a file named "NAE.jar"

Running:
The following is the syntax for running NAE from the command line, assuming we are in the NetworkAnalysisEngine directory:
>java -jar NAE.jar  <solution limit> <model file path> <observation file path> <mode>

<Solution limit> is the number of solutions to search for
<model file path> is a path to a model file ending in .net
<observation file path> is a path to a spec file ending in .spec or .cltspec or .ltlspec
<mode> is the mode of encoding in NuSMV. Current modes are:
    time_step:                     for use with .spec files, 
    temporal_logic_bmc:      for use with .ctlspec and .ltlspec files to run the SAT solver with bounded model checking
    temporal_logic_bdd:       for use with .ctlspec and .ltlspec files to use the BDD algorithms for verification
    ctl:                                currently under development, but theoritcally more optomized for .ctlspec files

additionally there are optional arguments, which, if specified, must be after the 4 required arguments. They are:
-v to perform validation on solutions 
-bmc <length> to specify the bounds of bmc. Default is 20.

Validation is currently only supported on solutions from time_step mode.

Test models:
In the NetworkAnalysisEngine directory are 3 subdirectories named test_models, LTL, and CTL, containing network (.net) and specification files (.spec/.ltlspec/.ctlspec) that we tested on, as well as .smv files generated by NAE (which are not intended to be human readable).


The test models in the testModels directory are meant to be run in time_step mode. Many of the included examples outperformed RE:IN on benchmarks. 

The test models in the CTL directory are meant to be run in temporal_logic_bdd mode (NuSMV does not support BMC based verification of CTL). One of the models included demonstrates the
usefulness of  CTL for asyncranous models, and is able to specify constraints on different possible paths that the non-deterministic asyncranous model can take.

The test models in the LTL directory can be run in either temporal_logic_bdd mode or temporal_logic_bmc mode, although the latter generally performs better than the former.
Included is a model that demonstrate the complex specifications LTL is capable of, as well as models that demonstrate how translation of RE:IN time-step style specs into LTL can sometimes result in a
performance boost (contrast the pluripotency_model10 under timestep mode with its LTL translation pluripotency10_ltl).

Source Code:
The complete source code for the tool can be found in the NAE directory, containing the code for the main tool, and the validate directory, containing the source for the validation component.

Understanding the output:
when NAE finishes running, it prints out all the solutions it finds. Solutions are numbered 0 - n-1 and are columns where each row is the name of an uncertain connection between 2 genes.
NAE either marks every optional connection as on or off in each solution. Here is an example output with 8 solutions:
                   0  1  2  3  4  5  6  7
             B->C :■  ■  ■  ■  ■  ■  ■  ■
             B->A :■  ■        ■        ■
             A->B :            ■  ■  ■  ■
             A->C :   ■     ■        ■  ■ 


Evaluating the tool:

Included in the NetworkAnalysisEngine directory is a bash script named "test" that builds the tool and runs all of the test models under various parameters, printing the results and providing benchmarks. 
Please note that some of the very large models take up alot of memory and may not run properly if the virtual machine has less than 10 GB of memory. Also note that some of the benchmarks obtained will be slightly slower on the VM than had NAE been run on a regular machine.
Make sure the terminal window is opened to fullscreen for proper formatting.
the bash script should be run by invoking: 
> bash test

Also included in the NetworkAnalsisEngine directory is a file "benchmark.test" that contains benchmarks for all the models when run on a  machine with the following specs:
64 bit Windows 
16 GB RAM
Processor: Inter Core i7-7700HQ    2.80   GHz

Interpetting the benchmarks:
The benchmarks obtained from the models in the testModel directory are interesting in that they are competitive with RE:IN, in fact usually they are faster.
The benchmarks from the models in the LTL and CTL directories cannot be compared to RE:IN, as they contain specififcations not possible in RE:IN. 
The exception to this is the pluripotency10_ltl model, which is a temporal logic translation of a RE:IN model that demonstrates how such a translation can improve performance (as compared to the prupotency_model10 which is the same specification but in RE:IN timestep style).


Running NAE without the bashscript:
To aid in running the tool directly to see how it works, the following are a bunch of ready to go commands to run NAE from a terminal open to the NetworkAnalysisEngine directory. They can be run as is or modified as the evaluator sees fit.


Running timestep models:
java -jar NAE.jar 100 TestModels/toy_model/model.net TestModels/toy_model/observations.spec time_step
java -jar NAE.jar 1 TestModels/minimal_pl/model.net TestModels/minimal_pl/observations.spec time_step
java -jar NAE.jar 1 TestModels/pluripotency_model/model.net TestModels/pluripotency_model/observation.spec time_step
java -jar NAE.jar 1 TestModels/pluripotency_modified/model.net TestModels/pluripotency_modified/observations.spec time_step
java -jar NAE.jar 10 TestModels/myloid_model/model.net TestModels/myloid_model/observations.spec time_step
java -jar NAE.jar 10 TestModels/pluripotency_model10/model.net TestModels/pluripotency_model10/observation.spec time_step

Running CTL models:
java -jar NAE.jar 100 CTL/toy_model_ctl/model.net CTL/toy_model_ctl/observations.ctlspec temporal_logic_bdd
java -jar NAE.jar 25 CTL/asyncMultiplePathExample/model.net CTL/asyncMultiplePathExample/observations.ctlspec temporal_logic_bdd



Running LTL models:
java -jar NAE.jar 100 LTL/toy_model_ltl/model.net LTL/toy_model_ltl/observations.ltlspec temporal_logic_bdd
java -jar NAE.jar 100 LTL/toy_model_ltl/model.net LTL/toy_model_ltl/observations.ltlspec temporal_logic_bmc -bmc 20
java -jar NAE.jar 10 LTL/pluripotency10_ltl/model.net LTL/pluripotency10_ltl/observation.ltlspec temporal_logic_bmc
java -jar NAE.jar 25 LTL/ComplexLTLExample/model.net LTL/ComplexLTLExample/observation.ltlspec temporal_logic_bmc