完成区间算术 + milp。

README.md

@@ -1,8 +1,23 @@
 # FFNN-Verify
-一个全连接ReLU节点的前馈神经网络的形式化验证器
+一个全连接ReLU节点的前馈神经网络的形式化验证器。使用了区间传播 + 混合整形线性规划两种方法进行神经网络验证。
+
+- [FFNN-Verify](#ffnn-verify)
+  - [1.1. dependence：](#11-dependence)
+  - [1.2. example:](#12-example)
 
 ---
 
-dependence：
+## 1.1. dependence：
 - numpy
-- mip
+- gurobi
+- keras
+
+
+## 1.2. example:
+本项目以ACAS XU为例，检查了属性3在网络1_1到1_9下的验证结果。
+
+```
+python main.py --npath /Acas/acas_1_1.h5 --type rea --prop 3
+```
+
+如果要验证其他属性，请自行编写输出约束的反例。

src/Layer.py

@@ -1,8 +1,5 @@
-from numpy import ndarray
 import numpy as np
-class L:
-    def __init__(self):
-        pass
+from numpy import ndarray
 
 
 class Layer:

src/networkClass.py

@@ -1,10 +1,10 @@
-import numpy as np
-from keras.models import load_model
 import keras
+import numpy as np
 from Layer import Layer
-from property import getNormaliseInput
 from typing import List
 from numpy import ndarray
+from keras.models import load_model
+from property import getNormaliseInput
 
 
 class Network:

src/solverClass.py

@@ -1,9 +1,9 @@
-from networkClass import Network
 import numpy as np
 import gurobipy as gp
-from gurobipy import GRB
 from Layer import Layer
 from typing import List
+from gurobipy import GRB
+from networkClass import Network
 
 class Solver:
     def __init__(self, network: Network, propertyFile: str):