Add requirements.txt to allow installing all dependencies. Fix GLPK p…

…ath issue by assumming that command line tool is installed.

README.md

@@ -17,7 +17,7 @@ See [nn_dependability_kit_manual.pdf](https://github.com/dependable-ai/nn-depend
 
 Examples are presented as jupyter notebooks to allow step-by-step understanding over the concepts. 
 
-- [Metrics & test case generation] GTSRB_Neuron2ProjectionCoverage_TestGen.ipynb, or GTSRB_AdditionalMetrics.ipynb, or KITTI_Scenario_Coverage.ipynb, or MNIST_Neuron2ProjectionCoverage_TestGen.ipynb, or SSD_InterpretationPrecision.ipynb
+- [Metrics & test case generation] GTSRB_Neuron2ProjectionCoverage_TestGen.ipynb, or GTSRB_AdditionalMetrics.ipynb, or Scenario_Coverage_A9.ipynb, or KITTI_Scenario_Coverage.ipynb, or MNIST_Neuron2ProjectionCoverage_TestGen.ipynb, or SSD_InterpretationPrecision.ipynb
 - [Formal verification] TargetVehicleProcessingNetwork_FormalVerification.ipynb
 - [Runtime verification] GTSRB_RuntimeMonitoring.ipynb, or MNIST_RuntimeMonitoring.ipynb  
 
@@ -35,9 +35,14 @@ There are four packages under nndependability, namely
 - PyTorch + Numpy + matplotlib + jupyter
 - [Test case generation] [Google optimization research tools](https://developers.google.com/optimization/introduction/installing/binary)
 - [Verification / static analysis] PuLP (python-based MILP connector to CBC and other solvers)
-    - [For Ubuntu users] CBC solver pre-shipped with PuLP may crash in solving some problems. Therefore, please additionally install [GNU GLPK](http://www.gnu.org/software/glpk/). The static analysis engine assumes that the GLPK solver is installed in the default directory "/usr/local/bin/glpsol". Whenever CBC crashes, GLPK is automatically triggered as a replacement. Unfortunately, this can't guarantee that both two solvers won't crash at the same time. Therefore, for industrial usage we strongly advise to use IBM CPLEX as the underlying MILP solver. 
+    - CBC solver pre-shipped with PuLP may crash in solving some problems. The static analysis engine assumes that the GLPK solver can be called (please set up PATH variable), such that whenever CBC crashes, GLPK is automatically triggered as a replacement. Unfortunately, this can't guarantee that both two solvers won't crash at the same time. Therefore, for industrial usage we strongly advise to use IBM CPLEX as the underlying MILP solver. 
+		- [GNU GLPK] http://www.gnu.org/software/glpk/
+		- [GPLK on Windows] http://winglpk.sourceforge.net/
+
 - [Run-time verification] dd (binary decision diagram implemented using python)
 
+Use Requirements.txt to install dependencies to run most of the notebooks (excluding Tensorflow).
+
 ## Related publications
 
 - [Metrics & test case generation] https://arxiv.org/abs/1806.02338

manual_latex/main.tex

@@ -7,7 +7,7 @@
 
 \title{\textsf{nn-dependability-kit} manual \\ \begin{large}(Public version)\end{large}}
 
-\date{February 13th, 2019}
+\date{April 23th, 2019}
 
 \usepackage{natbib}
 \usepackage{graphicx}
@@ -33,14 +33,21 @@ \section{Availability and License}
 
 \section{Dependencies and Installation}
 
-Here we list dependencies of $\textsf{nn-dependability-kit}$:
+Here we list some important dependencies of $\textsf{nn-dependability-kit}$\footnote{Users can simply use Requirements.txt to install dependencies to run most of the notebooks (excluding Tensorflow).}:
+
+
 \begin{description}
 \item[(Basics)] \texttt{PyTorch} + \texttt{Numpy} + \texttt{matplotlib} + \texttt{jupyter}. 
 \item[(Test case generation)] Google optimization research tools, available at \\ {\small\url{https://developers.google.com/optimization/introduction/installing/binary}}
 
 \item[(Verification / static analysis)] \texttt{PuLP} (python-based MILP connector to Coin-or branch and cut (CBC) solver and other solvers)
 \begin{itemize}
-    \item For Ubuntu users, the CBC solver shipped with PuLP may crash in solving some problems. Therefore, please additionally install GNU GLPK. The static analysis engine assumes that the GLPK solver is installed in the default directory "\texttt{/usr/local/bin/glpsol}". Whenever CBC solver crashes, GLPK solver is automatically triggered as a replacement.
+    \item The CBC solver shipped with PuLP may crash in solving some problems. Therefore, please additionally install GNU GLPK. The static analysis engine assumes that the GLPK solver can be called anywhere with PATH variable properly set. Whenever CBC solver crashes, GLPK solver is automatically triggered as a replacement.
+    \begin{description}
+    	\item[Ubuntu] \url{http://www.gnu.org/software/glpk/}
+    	\item[Windows] \url{http://winglpk.sourceforge.net/}
+    \end{description}
+
     \item For academic users, we strongly advise to use IBM CPLEX as the underlying solver, as academic partners can retrieve IBM CPLEX for free. For open source solvers, we have experienced multiple times unexpected crashes. Even the above workaround cannot guarantee a crash-free behavior. 
 \end{itemize}
 \item[(Run-time verification)] \texttt{dd} (binary decision diagram implemented using python)
@@ -49,6 +56,7 @@ \section{Dependencies and Installation}
 \textsf{nn-dependability-kit} mainly supports PyTorch. For TensorFlow, the support is currently restricted to formal verification. However, as the input for computing the metrics and the input for building monitors uses numpy arrays rather than native pytorch tensors, it is very easy to use these metrics or to build runtime monitors also with TensorFlow. 
 
 
+
 \section{Examples}
 
 Within the source code of \textsf{nn-dependability-kit}, examples are presented as jupyter notebooks to allow step-by-step execution with explanations written as markdown languages.  

nndependability/formal/octagon.py

@@ -125,7 +125,8 @@ def deriveReLuOutputOctagonBound(isMaxBound, layerIndex, weights, bias, numberOf
         try:
             prob.solve()
         except: 
-            prob.solve(GLPK("/usr/local/bin/glpsol", options=["--cbg"]))
+            prob.solve(GLPK(options=["--cbg"]))
+			#prob.solve(GLPK("/usr/local/bin/glpsol", options=["--cbg"]))
     else:
         prob.solve(CPLEX())
 

requirements.txt

@@ -0,0 +1,65 @@
+astutils==0.0.3
+attrs==19.1.0
+backcall==0.1.0
+bleach==3.1.0
+colorama==0.4.1
+cycler==0.10.0
+dd==0.5.4
+decorator==4.4.0
+defusedxml==0.6.0
+entrypoints==0.3
+ipykernel==5.1.0
+ipython==7.4.0
+ipython-genutils==0.2.0
+ipywidgets==7.4.2
+jedi==0.13.3
+Jinja2==2.10.1
+jsonschema==3.0.1
+jupyter==1.0.0
+jupyter-client==5.2.4
+jupyter-console==6.0.0
+jupyter-core==4.4.0
+kiwisolver==1.0.1
+MarkupSafe==1.1.1
+matplotlib==3.0.3
+mistune==0.8.4
+nbconvert==5.4.1
+nbformat==4.4.0
+networkx==2.3
+notebook==5.7.8
+numpy==1.16.3
+opencv-python==4.1.0.25
+ortools==7.0.6546
+pandas==0.24.2
+pandocfilters==1.4.2
+parso==0.4.0
+pickleshare==0.7.5
+Pillow==6.0.0
+ply==3.10
+prometheus-client==0.6.0
+prompt-toolkit==2.0.9
+protobuf==3.7.1
+psutil==5.6.1
+PuLP==1.6.9
+pydot==1.4.1
+Pygments==2.3.1
+pyparsing==2.4.0
+pyrsistent==0.14.11
+python-dateutil==2.8.0
+pytz==2019.1
+pywinpty==0.5.5
+pyzmq==18.0.1
+qtconsole==4.4.3
+scipy==1.2.1
+seaborn==0.9.0
+Send2Trash==1.5.0
+six==1.12.0
+terminado==0.8.2
+testpath==0.4.2
+torch==1.0.1
+torchvision==0.2.2.post3
+tornado==6.0.2
+traitlets==4.3.2
+wcwidth==0.1.7
+webencodings==0.5.1
+widgetsnbextension==3.4.2