Getting Started Guide
Alloy models used in paper are stored under datasets/alloy-models directory, where both models with and without symmetry breaking are included. Datasets generated using the Alloy models are stored in csv files under datasets/csv directory.
Alloy generated ground-truth Conjunctive Normal Form (CNF) formulas are in datasets/cnf directory. There are two sub-directories for two sizes of scopes. Directory large contains CNF formulas with a big scope (as shown in Table 1 of Submitted Paper), directory small contains CNF formulas for a smaller scope.
The datasets/accmc directory contains the CNF formulas for the ~AccMC, which quantifies the accuracy of trained ML models with respect to ground truth formulas. There are 4 sub-directories: (1) groundoff_treeoff, containing CNF files when ground truth is without symmetry breaking constraints and decision tree was trained on datasets generated by turning symmetry breaking Off; (2) groundoff_treeon, containing CNF files when ground truth is without symmetry breaking constraints and decision tree was trained on datasets generated by turning symmetry breaking On; (3) groundon_treeoff, containing CNF files when ground truth has symmetry breaking constraints and decision tree was trained on datasets generated by turning symmetry breaking Off; and (4) groundon_treeon, containing CNF files when ground truth has symmetry breaking constraints and decision tree was trained on datasets generated by turning symmetry breaking On. The file names follow the naming convention label_property.cnf (e.g., tf_equivalence.cnf refers to the case when equivalence property was satisfied but decision tree predicted the label false). These CNF formulas will be regenerated using the commands presented at end of document.
The datasets/diffmc directory contains CNF formulas for ~DiffMC, which quantifies the semantic differences between the two trained models. There are two subdirectories: (1) treeon_treeon, containing CNF files when decision trees were trained on dataset generated using symmetry breaking; and (2) treeoff_treeoff, containing CNF files of tree when decision trees were generated on datasets without symmetry breaking. The file names follow the naming convention label_property.cnf (e.g., tf_equivalence.cnf refers to the case when one tree predicted the label true and other predicted the label false). These CNF formulas will be regenerated using the commands presented at end of document.
- linux OS (Ubuntu)
- python3
- pydotplus
- numpy
- sklearn
- matplotlib
You can install one using pip package manager, e.g.:
- pip3 install pydotplus numpy sklearn matplotlib
Download projMC executable file from http://www.cril.univ-artois.fr/kc/projmc.html
- Keep the downloaded file inside modelcounter directory.
- Run sudo chmod +x modelcounter/projMC_linux to give execution permissions to model counter.
Note: All commands should be run inside artifact directory.
- To reproduce results of the Table 2 from the paper, you can run the
following command:
- python table2.py partialorder
- This command trains and evaluates a decision tree on the Alloy dataset stored in datasets/csv/Sym-Brk-On/partialorder.csv. We ensure that the same decision tree is always learned by setting the random seed to a fixed value.
- Tables generated correspond to tables 16-31 in Appendix.
- To reproduce results of the Table 3 from the paper, you can run the
following command:
- python3 table3.py partialorder
- Tables generated correspond to tables 9 in Appendix.
- To reproduce results of the Table 4 from the paper, you can run the
following command:
- python table4.py partialorder
- This command trains and evaluates a decision tree on the Alloy dataset stored in datasets/csv/Sym-Brk-Off/partialorder.csv. We ensure that the same decision tree is always learned by setting the random seed to a fixed value.
- Tables generated correspond to tables 32-47 in Appendix.
- To reproduce results of the Table 5 from the paper, you can run the
following command:
- python3 table5.py partialorder
- Tables generated correspond to tables 12 in Appendix.
- To reproduce results of the Table 6 from the paper, you can run the
following command:
- python3 table6.py partialorder
- Tables generated correspond to tables 10 in Appendix.
- To reproduce results of the Table 7 from the paper, you can run the
following command:
- python3 table7.py partialorder
- Tables generated correspond to tables 11 in Appendix.
- To reproduce results of the Table 8 from the paper, you can run the
following command:
- python3 table8.py partialorder
- Tables generated correspond to tables 14 in Appendix.
- More generally, you can run the same experiment for other properties: {antisymmetric, bijective, connex, equivalence, function, functional, injective, irreflexive, nonstrictorder, partialorder, preorder, reflexive, strictorder, surjective, totalorder, transitive}.
The experiment time for each property is shown in each table in main paper.
- To reproduce results of the Table 2 from the paper, you can run the
following command:
- python table2all.py
- This command trains and evaluates a decision tree on the Alloy datasets stored in datasets/csv/Sym-Brk-On/.csv. We ensure that the same decision tree is always learned by setting the random seed to a fixed value.
- Tables generated correspond to tables 16-31 in Appendix.
- To reproduce results of the Table 3 from the paper, you can run the
following command:
- python3 table3all.py
- Tables generated correspond to tables 9 in Appendix.
- To reproduce results of the Table 4 from the paper, you can run the
following command:
- python3 table4all.py
- This command trains and evaluates a decision tree on the Alloy datasets stored in datasets/csv/Sym-Brk-Off/.csv. We ensure that the same decision tree is always learned by setting the random seed to a fixed value.
- Tables generated correspond to tables 32-47 in Appendix.
- To reproduce results of the Table 5 from the paper, you can run the
following command:
- python3 table5all.py
- Tables generated correspond to tables 12 in Appendix.
- To reproduce results of the Table 6 from the paper, you can run the
following command:
- python3 table6all.py
- Tables generated correspond to tables 10 in Appendix.
- To reproduce results of the Table 7 from the paper, you can run the
following command:
- python3 table7all.py
- Tables generated correspond to tables 11 in Appendix.
- To reproduce results of the Table 8 from the paper, you can run the
following command:
- python3 table8all.py
- Tables generated correspond to tables 14 in Appendix.