[exps] Uniformize and organize new models

examples/mnist/nets/dummy_nn/train.py

@@ -15,14 +15,14 @@ from torchvision import transforms
 img_size = 14
 
 SEED = 42
-STATE_PATH = f"{img_size}x{img_size}_FNN_s{SEED}.pth"
-ONNX_PATH = f"{img_size}x{img_size}_FNN_s{SEED}.onnx"
-PRUNED_MODEL_PATH = f"pruned_{img_size}x{img_size}_FNN_s{SEED}.pkl"
-PRUNED_ONNX_PATH = f"pruned_{img_size}x{img_size}_FNN_s{SEED}.onnx"
-FNN_PRE_PATH = f"fnn_pre_s{SEED}.pth"
-FNN_PRE_ONNX_PATH = f"fnn_pre_s{SEED}.onnx"
-FNN_POST_PATH = f"fnn_post_s{SEED}.pth"
-FNN_POST_ONNX_PATH = f"fnn_post_s{SEED}.onnx"
+STATE_PATH = f"FNN_{img_size}x{img_size}_s{SEED}.pth"
+ONNX_PATH = f"FNN_{img_size}x{img_size}_s{SEED}.onnx"
+PRUNED_MODEL_PATH = f"FNN_{img_size}x{img_size}_pruned_s{SEED}.pkl"
+PRUNED_ONNX_PATH = f"FNN_{img_size}x{img_size}_pruned_s{SEED}.onnx"
+FNN_PRE_PATH = f"FNN_28x28_pre_s{SEED}.pth"
+FNN_PRE_ONNX_PATH = f"FNN_28x28_pre_s{SEED}.onnx"
+FNN_POST_PATH = f"FNN_28x28_post_s{SEED}.pth"
+FNN_POST_ONNX_PATH = f"FNN_28x28_post_s{SEED}.onnx"
 
 torch.manual_seed(SEED)
 

tests/check_pruning.t

@@ -4,4 +4,4 @@
   acasxu
   mnist
 
-#  $ caisar verify --prover PyRAT  --ltag=StackTrace --define model_filename:nets/dummy_nn/FNN_s42.onnx --define pruned_model_filename:nets/dummy_nn/pruned_FNN_s42.onnx --define dataset_filename:csv/single_image.csv ../examples/mnist/check_pruning.mlw -v
+#  $ caisar verify --prover PyRAT  --ltag=StackTrace --define model_filename:nets/pruned/FNN_28x28_s42.onnx --define pruned_model_filename:nets/pruned/FNN_28x28_pruned_s42.onnx --define dataset_filename:csv/single_image.csv ../examples/mnist/check_pruning.mlw -v

tests/dune

@@ -36,8 +36,8 @@
   (glob_files bin/*)
   filter_tmpdir.sh
   ../examples/mnist/check_pruning.mlw
-  ../examples/mnist/nets/dummy_nn/FNN_s42.onnx
-  ../examples/mnist/nets/dummy_nn/pruned_FNN_s42.onnx
+  ../examples/mnist/nets/pruned/FNN_28x28_s42.onnx
+  ../examples/mnist/nets/pruned/FNN_28x28_pruned_s42.onnx
   ../examples/mnist/csv/single_image.csv
   )
  (package caisar))
@@ -51,8 +51,8 @@
   (glob_files bin/*)
   filter_tmpdir.sh
   ../examples/mnist/splitted_nn.mlw
-  ../examples/mnist/nets/dummy_nn/fnn_pre_s42.onnx
-  ../examples/mnist/nets/dummy_nn/fnn_post_s42.onnx
+  ../examples/mnist/nets/splitted/FNN_28x28_pre_s42.onnx
+  ../examples/mnist/nets/splitted/FNN_28x28_post_s42.onnx
   ../examples/mnist/csv/single_image.csv
   )
  (package caisar))

tests/splitted_nn.t

@@ -4,4 +4,4 @@
   acasxu
   mnist
 
-#  $ caisar verify --prover PyRAT  --ltag=StackTrace --define pre_model_filename:nets/dummy_nn/fnn_pre_s42.onnx --define post_model_filename:nets/dummy_nn/fnn_post_s42.onnx --define dataset_filename:csv/single_image.csv ../examples/mnist/splitted_nn.mlw -v
+#  $ caisar verify --prover PyRAT  --ltag=StackTrace --define pre_model_filename:nets/splitted/FNN_28x28_pre_s42.onnx --define post_model_filename:nets/splitted/FNN_28x28_post_s42.onnx --define dataset_filename:csv/single_image.csv ../examples/mnist/splitted_nn.mlw -v