Changes

              
    

          
          
        
        

            
f
1
{
f
1
{
            
2
  "author": "Teuber, Samuel",
2
  "author": "Teuber, Samuel",
            
3
  "author_email": "",
3
  "author_email": "",
            
4
  "creator_user_id": "17755db4-395a-4b3b-ac09-e8e3484ca700",
4
  "creator_user_id": "17755db4-395a-4b3b-ac09-e8e3484ca700",
            
5
  "doi": "10.35097/1520",
5
  "doi": "10.35097/1520",
            
6
  "doi_date_published": "2023",
6
  "doi_date_published": "2023",
            
7
  "doi_publisher": "",
7
  "doi_publisher": "",
            
8
  "doi_status": "True",
8
  "doi_status": "True",
            
9
  "extra_authors": [
9
  "extra_authors": [
            
10
    {
10
    {
            
11
      "extra_author": "Weigl, Alexander",
11
      "extra_author": "Weigl, Alexander",
            
12
      "orcid": "0000-0001-8446-4598"
12
      "orcid": "0000-0001-8446-4598"
            
13
    }
13
    }
            
14
  ],
14
  ],
            
15
  "groups": [],
15
  "groups": [],
            
16
  "id": "5198ee06-8405-4485-9d8f-419ed45f9189",
16
  "id": "5198ee06-8405-4485-9d8f-419ed45f9189",
            
17
  "isopen": false,
17
  "isopen": false,
            
18
  "license_id": "Other",
18
  "license_id": "Other",
            
19
  "license_title": "Other",
19
  "license_title": "Other",
            
20
  "metadata_created": "2023-08-04T08:50:58.614879",
20
  "metadata_created": "2023-08-04T08:50:58.614879",
            
t
21
  "metadata_modified": "2023-08-04T08:50:58.614885",
t
21
  "metadata_modified": "2023-08-04T08:52:08.623910",
            
22
  "name": "rdr-doi-10-35097-1520",
22
  "name": "rdr-doi-10-35097-1520",
            
23
  "notes": "TechnicalRemarks: # `counterSharp` Experiment and Play 
23
  "notes": "TechnicalRemarks: # `counterSharp` Experiment and Play 
            
24
Environment\r\n\r\nThis repository contains the reproducible 
24
Environment\r\n\r\nThis repository contains the reproducible 
            
25
experimental evaluation of the [counterSharp 
25
experimental evaluation of the [counterSharp 
            
26
tool](https://github.com/samysweb/counterSharp).\r\nThe repository 
26
tool](https://github.com/samysweb/counterSharp).\r\nThe repository 
            
27
contains a Docker file which configures the counterSharp tool, two 
27
contains a Docker file which configures the counterSharp tool, two 
            
28
model counters (ApproxMC and Ganak) as well as the [tool by Dimovski 
28
model counters (ApproxMC and Ganak) as well as the [tool by Dimovski 
            
29
et al.](https://github.com/aleksdimovski/probab_analyzer) for our 
29
et al.](https://github.com/aleksdimovski/probab_analyzer) for our 
            
30
experiments.\r\nFurthermore the repository contains the benchmarks on 
30
experiments.\r\nFurthermore the repository contains the benchmarks on 
            
31
which we ran our experiments as well as the logs of our experiments 
31
which we ran our experiments as well as the logs of our experiments 
            
32
and scripts for transforming the log files into LaTeX 
32
and scripts for transforming the log files into LaTeX 
            
33
tables.\r\n\r\n## Getting Started\r\n\r\nIn order to pull and run the 
33
tables.\r\n\r\n## Getting Started\r\n\r\nIn order to pull and run the 
            
34
docker container from docker hub you should execute `docker run`. 
34
docker container from docker hub you should execute `docker run`. 
            
35
\r\nOr, you can load the archived and evaluated artifact into docker 
35
\r\nOr, you can load the archived and evaluated artifact into docker 
            
36
with\r\n```\r\ndocker load < 
36
with\r\n```\r\ndocker load < 
            
37
countersharp-experiments.tar.gz\r\n```\r\n\r\nIf the image is loaded, 
37
countersharp-experiments.tar.gz\r\n```\r\n\r\nIf the image is loaded, 
            
38
`docker run` opens a shell allowing the execution of further 
38
`docker run` opens a shell allowing the execution of further 
            
39
commands:\r\n\r\n```bash\r\ndocker run -it -v 
39
commands:\r\n\r\n```bash\r\ndocker run -it -v 
            
40
`pwd`/results:/experiments/results 
40
`pwd`/results:/experiments/results 
            
41
samweb/countersharp-experiments\r\n```\r\n\r\nBy using a volume, the 
41
samweb/countersharp-experiments\r\n```\r\n\r\nBy using a volume, the 
            
42
results are written to the host system rather than the docker 
42
results are written to the host system rather than the docker 
            
43
container\r\nYou can remove the volume mounting option (`-v ...`), and 
43
container\r\nYou can remove the volume mounting option (`-v ...`), and 
            
44
create `/experiments/results` inside the container if you can spare 
44
create `/experiments/results` inside the container if you can spare 
            
45
the results.\r\nIf you are using the volume and run into permission 
45
the results.\r\nIf you are using the volume and run into permission 
            
46
problems, then you need to give rights via SELinux: `chcon -Rt 
46
problems, then you need to give rights via SELinux: `chcon -Rt 
            
47
svirt_sandbox_file_t `pwd`/results`.\r\n\r\nThis will create a 
47
svirt_sandbox_file_t `pwd`/results`.\r\n\r\nThis will create a 
            
48
writable folder `results` in your current folder which will hold any 
48
writable folder `results` in your current folder which will hold any 
            
49
logs from experiments. \r\n\r\n\r\nA minimal example can be executed 
49
logs from experiments. \r\n\r\n\r\nA minimal example can be executed 
            
50
by running (this takes approximately **70 
50
by running (this takes approximately **70 
            
51
seconds**):\r\n```bash\r\n./showcase.sh\r\n```\r\nThis will create 
51
seconds**):\r\n```bash\r\n./showcase.sh\r\n```\r\nThis will create 
            
52
benchmark log files for the benchmarks `for_bounded_loop1.c` and 
52
benchmark log files for the benchmarks `for_bounded_loop1.c` and 
            
53
`overflow.c` in the folder [`results`](results).\r\nFor example, 
53
`overflow.c` in the folder [`results`](results).\r\nFor example, 
            
54
`/experiments/results/for_bounded_loop1.c/0X/` contains five folder 
54
`/experiments/results/for_bounded_loop1.c/0X/` contains five folder 
            
55
for the five repeated runs of the experiments on this file. \r\nEach 
55
for the five repeated runs of the experiments on this file. \r\nEach 
            
56
folder `/experiments/results/for_bounded_loop1.c/0X/` contains the 
56
folder `/experiments/results/for_bounded_loop1.c/0X/` contains the 
            
57
folders for the different tools, which includes the log and output 
57
folders for the different tools, which includes the log and output 
            
58
files.\r\n\r\n\r\nA full run can be executed by running (this takes 
58
files.\r\n\r\n\r\nA full run can be executed by running (this takes 
            
59
approximately a little under **2 
59
approximately a little under **2 
            
60
days**):\r\n```bash\r\n./run-all.sh\r\n```\r\n\r\nAdditionally single 
60
days**):\r\n```bash\r\n./run-all.sh\r\n```\r\n\r\nAdditionally single 
            
61
benchmarks can be executed through the following 
61
benchmarks can be executed through the following 
            
62
commands:\r\n```bash\r\nrun-instance approx program.c \"[counterSharp 
62
commands:\r\n```bash\r\nrun-instance approx program.c \"[counterSharp 
            
63
arguments]\" # Runs countersharp with ApproxMC on 
63
arguments]\" # Runs countersharp with ApproxMC on 
            
64
program.c\r\nrun-instance ganak program.c \"[counterSharp arguments]\" 
64
program.c\r\nrun-instance ganak program.c \"[counterSharp arguments]\" 
            
65
# Runs countersharp with Ganak on program.c\r\nProbab.native -single 
65
# Runs countersharp with Ganak on program.c\r\nProbab.native -single 
            
66
-domain polyhedra program.c # Runs the tool by Dimovski et al. for 
66
-domain polyhedra program.c # Runs the tool by Dimovski et al. for 
            
67
deterministic programs\r\nProbab.native -single -domain polyhedra 
67
deterministic programs\r\nProbab.native -single -domain polyhedra 
            
68
-nondet program.c # Runs the tool by Dimovski et al. for 
68
-nondet program.c # Runs the tool by Dimovski et al. for 
            
69
nondeterministic programs\r\n```\r\nFor example we can execute 
69
nondeterministic programs\r\n```\r\nFor example we can execute 
            
70
`run-instance approx /experiments/benchmarks/confidence.c \"--function 
70
`run-instance approx /experiments/benchmarks/confidence.c \"--function 
            
71
testfun --unwind 1\"` to obtain the outcome of counterSharp and 
71
testfun --unwind 1\"` to obtain the outcome of counterSharp and 
            
72
ApproxMC for the benchmark `confidence.c`.\r\nNote that the time 
72
ApproxMC for the benchmark `confidence.c`.\r\nNote that the time 
            
73
information produced by runlim is always only for one part of the 
73
information produced by runlim is always only for one part of the 
            
74
entire execution (i.e. for counterSharp or  one ApproxMC run or one 
74
entire execution (i.e. for counterSharp or  one ApproxMC run or one 
            
75
Ganak run). The script `run-instance` is straightforwarded, we have 
75
Ganak run). The script `run-instance` is straightforwarded, we have 
            
76
the call to our tool 
76
the call to our tool 
            
77
](https://github.com/samysweb/counterSharp):\r\n\r\n```bash\r\npython3 
77
](https://github.com/samysweb/counterSharp):\r\n\r\n```bash\r\npython3 
            
78
-m counterSharp --amm /tmp/amm.dimacs --amh /tmp/amh.dimacs --asm 
78
-m counterSharp --amm /tmp/amm.dimacs --amh /tmp/amh.dimacs --asm 
            
79
/tmp/asm.dimacs --ash /tmp/ash.dimacs --con /tmp/con.dimacs -d $3 
79
/tmp/asm.dimacs --ash /tmp/ash.dimacs --con /tmp/con.dimacs -d $3 
            
80
$2\r\n```\r\nwhich is followed by the call of `ApproxMC` oder 
80
$2\r\n```\r\nwhich is followed by the call of `ApproxMC` oder 
            
81
`ganak`.\r\n\r\n\r\n\r\n## Benchmarks\r\nThe benchmarks are contained 
81
`ganak`.\r\n\r\n\r\n\r\n## Benchmarks\r\nThe benchmarks are contained 
            
82
in the folder [`benchmarks`](benchmarks) which also includes an 
82
in the folder [`benchmarks`](benchmarks) which also includes an 
            
83
overview on the sources and modifications to the benchmarks  \r\nNote 
83
overview on the sources and modifications to the benchmarks  \r\nNote 
            
84
that benchmark versions for the tool by Dimovski et al. are contained 
84
that benchmark versions for the tool by Dimovski et al. are contained 
            
85
in folder [`benchmarks-dimovski`](benchmarks-dimovski)\r\n\r\n## 
85
in folder [`benchmarks-dimovski`](benchmarks-dimovski)\r\n\r\n## 
            
86
Benchmark Results\r\nThe results are contained in the folder 
86
Benchmark Results\r\nThe results are contained in the folder 
            
87
[`results`](results) in which all logs from benchmark runs 
87
[`results`](results) in which all logs from benchmark runs 
            
88
reside.\r\nThe log files from the evaluation are not available in the 
88
reside.\r\nThe log files from the evaluation are not available in the 
            
89
Docker Image, but just on GitHub.\r\nThe logs are split-up by 
89
Docker Image, but just on GitHub.\r\nThe logs are split-up by 
            
90
benchmark instance (first level folder), run number (second level 
90
benchmark instance (first level folder), run number (second level 
            
91
folder) and tool (third level folder)  \r\nFor example, the file 
91
folder) and tool (third level folder)  \r\nFor example, the file 
            
92
`results/bwd_loop1a.c/01/approxmc/stdout.log` contains the stdout and 
92
`results/bwd_loop1a.c/01/approxmc/stdout.log` contains the stdout and 
            
93
stderr of running approxmc on the instance `bwd_loop1a.c` in run `01`  
93
stderr of running approxmc on the instance `bwd_loop1a.c` in run `01`  
            
94
\r\n\r\n### Machine Details\r\nAll runs were executed on a Linux 
94
\r\n\r\n### Machine Details\r\nAll runs were executed on a Linux 
            
95
machine housing an Intel(R) Core(TM) i5-6500 CPU (3.20GHz) and 16GB of 
95
machine housing an Intel(R) Core(TM) i5-6500 CPU (3.20GHz) and 16GB of 
            
96
memory.\r\nNote that for every benchmark log 
96
memory.\r\nNote that for every benchmark log 
            
97
`01/counterSharp/init.log` contains information on the machine used 
97
`01/counterSharp/init.log` contains information on the machine used 
            
98
for benchmark execution as well as on the commits used in the 
98
for benchmark execution as well as on the commits used in the 
            
99
experiments.\r\n\r\n## Running benchmarks\r\nFor all cases of 
99
experiments.\r\n\r\n## Running benchmarks\r\nFor all cases of 
            
100
automated benchmark execution we assume a CSV file containing relevant 
100
automated benchmark execution we assume a CSV file containing relevant 
            
101
information on the instances to run: The first column is the 
101
information on the instances to run: The first column is the 
            
102
benchmark's name, the second column are parameters passed to 
102
benchmark's name, the second column are parameters passed to 
            
103
counterSharp (see `instances.csv`) or the tool by Dimovski (see 
103
counterSharp (see `instances.csv`) or the tool by Dimovski (see 
            
104
`instances-dimovski.csv`).\r\nAll scripts produce benchmarking results 
104
`instances-dimovski.csv`).\r\nAll scripts produce benchmarking results 
            
105
for \"missing\" instances, i.e. instances for which no folder can be 
105
for \"missing\" instances, i.e. instances for which no folder can be 
            
106
found in the `results` folder.\r\n\r\n- Run counterSharp on the 
106
found in the `results` folder.\r\n\r\n- Run counterSharp on the 
            
107
benchmarks:  \r\n`run-counterSharp instances.csv`\r\n- Run 
107
benchmarks:  \r\n`run-counterSharp instances.csv`\r\n- Run 
            
108
[ApproxMC](https://github.com/meelgroup/ApproxMC) on benchmarks:  
108
[ApproxMC](https://github.com/meelgroup/ApproxMC) on benchmarks:  
            
109
\r\n`run-approxmc instances.csv`\r\n - Only after counterSharp has 
109
\r\n`run-approxmc instances.csv`\r\n - Only after counterSharp has 
            
110
been run\r\n- Run [GANAK](https://github.com/meelgroup/ganak) on 
110
been run\r\n- Run [GANAK](https://github.com/meelgroup/ganak) on 
            
111
benchmarks:  \r\n`run-ganak instances.csv`\r\n - Only after 
111
benchmarks:  \r\n`run-ganak instances.csv`\r\n - Only after 
            
112
counterSharp has been run\r\n- Run [Dimovski's 
112
counterSharp has been run\r\n- Run [Dimovski's 
            
113
tool](https://github.com/aleksdimovski/probab_analyzer) on benchmarks:  
113
tool](https://github.com/aleksdimovski/probab_analyzer) on benchmarks:  
            
114
\r\n`run-dimovski instances-dimovski.csv`\r\n\r\n## Log 
114
\r\n`run-dimovski instances-dimovski.csv`\r\n\r\n## Log 
            
115
summarization\r\nSummarization is possible through the python script 
115
summarization\r\nSummarization is possible through the python script 
            
116
in `logParsing/parse.py` within the container.\r\nThe script takes as 
116
in `logParsing/parse.py` within the container.\r\nThe script takes as 
            
117
input a list of benchmarks to process and returns (parts of) a LaTeX 
117
input a list of benchmarks to process and returns (parts of) a LaTeX 
            
118
table.\r\nNote, that there must exist logs for all benchmarks provided 
118
table.\r\nNote, that there must exist logs for all benchmarks provided 
            
119
in the CSV file for the call to succeed!\r\n- **To obtain (sorted) 
119
in the CSV file for the call to succeed!\r\n- **To obtain (sorted) 
            
120
results for deterministic benchmarks:**  \r\n`cat 
120
results for deterministic benchmarks:**  \r\n`cat 
            
121
logParsing/deterministic-sorted.csv| python3 logParsing/parse.py 
121
logParsing/deterministic-sorted.csv| python3 logParsing/parse.py 
            
122
results aggregate2`\r\n- **To obtain (sorted) results for 
122
results aggregate2`\r\n- **To obtain (sorted) results for 
            
123
nondeterministic benchmarks:**  \r\n`cat 
123
nondeterministic benchmarks:**  \r\n`cat 
            
124
logParsing/nondeterministic-sorted.csv| python3 logParsing/parse.py 
124
logParsing/nondeterministic-sorted.csv| python3 logParsing/parse.py 
            
125
results nondet`\r\n\r\n## Building the docker container\r\nAll tools 
125
results nondet`\r\n\r\n## Building the docker container\r\nAll tools 
            
126
are packaged into a Dockerfile which makes any installation 
126
are packaged into a Dockerfile which makes any installation 
            
127
unnecessary.\r\nThere is, however, the need for a running Docker 
127
unnecessary.\r\nThere is, however, the need for a running Docker 
            
128
installation.\r\nThe `Dockerfile` build depends on the accessibility 
128
installation.\r\nThe `Dockerfile` build depends on the accessibility 
            
129
of the following GitHub Repositories:\r\n- 
129
of the following GitHub Repositories:\r\n- 
            
130
[CryptoMiniSat](https://github.com/msoos/cryptominisat)\r\n- 
130
[CryptoMiniSat](https://github.com/msoos/cryptominisat)\r\n- 
            
131
[ApproxMC](https://github.com/meelgroup/approxmc)\r\n- 
131
[ApproxMC](https://github.com/meelgroup/approxmc)\r\n- 
            
132
[Ganak](https://github.com/meelgroup/ganak)\r\n- 
132
[Ganak](https://github.com/meelgroup/ganak)\r\n- 
            
133
robab_Analyzer](https://github.com/aleksdimovski/probab_analyzer)\r\n- 
133
robab_Analyzer](https://github.com/aleksdimovski/probab_analyzer)\r\n- 
            
134
[counterSharp](https://github.com/samysweb/counterSharp)\r\n \r\nThe 
134
[counterSharp](https://github.com/samysweb/counterSharp)\r\n \r\nThe 
            
135
Docker image is hosted at 
135
Docker image is hosted at 
            
136
//hub.docker.com/repository/docker/samweb/countersharp-experiments).",
136
//hub.docker.com/repository/docker/samweb/countersharp-experiments).",
            
137
  "num_resources": 0,
137
  "num_resources": 0,
            
138
  "num_tags": 0,
138
  "num_tags": 0,
            
139
  "orcid": "",
139
  "orcid": "",
            
140
  "organization": {
140
  "organization": {
            
141
    "approval_status": "approved",
141
    "approval_status": "approved",
            
142
    "created": "2023-01-12T13:30:23.238233",
142
    "created": "2023-01-12T13:30:23.238233",
            
143
    "description": "RADAR (Research Data Repository) is a 
143
    "description": "RADAR (Research Data Repository) is a 
            
144
cross-disciplinary repository for archiving and publishing research 
144
cross-disciplinary repository for archiving and publishing research 
            
145
data from completed scientific studies and projects. The focus is on 
145
data from completed scientific studies and projects. The focus is on 
            
146
research data from subjects that do not yet have their own 
146
research data from subjects that do not yet have their own 
            
147
discipline-specific infrastructures for research data management. ",
147
discipline-specific infrastructures for research data management. ",
            
148
    "id": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
148
    "id": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
            
149
    "image_url": "radar-logo.svg",
149
    "image_url": "radar-logo.svg",
            
150
    "is_organization": true,
150
    "is_organization": true,
            
151
    "name": "radar",
151
    "name": "radar",
            
152
    "state": "active",
152
    "state": "active",
            
153
    "title": "RADAR",
153
    "title": "RADAR",
            
154
    "type": "organization"
154
    "type": "organization"
            
155
  },
155
  },
            
156
  "owner_org": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
156
  "owner_org": "013c89a9-383c-4200-8baa-0f78bf1d91f9",
            
157
  "private": false,
157
  "private": false,
            
158
  "production_year": "2021",
158
  "production_year": "2021",
            
159
  "publication_year": "2023",
159
  "publication_year": "2023",
            
160
  "publishers": [
160
  "publishers": [
            
161
    {
161
    {
            
162
      "publisher": "Karlsruhe Institute of Technology"
162
      "publisher": "Karlsruhe Institute of Technology"
            
163
    }
163
    }
            
164
  ],
164
  ],
            
165
  "relationships_as_object": [],
165
  "relationships_as_object": [],
            
166
  "relationships_as_subject": [],
166
  "relationships_as_subject": [],
            
167
  "repository_name": "RADAR (Research Data Repository)",
167
  "repository_name": "RADAR (Research Data Repository)",
            
168
  "resources": [],
168
  "resources": [],
            
169
  "services_used_list": "",
169
  "services_used_list": "",
            
170
  "source_metadata_created": "2023",
170
  "source_metadata_created": "2023",
            
171
  "source_metadata_modified": "",
171
  "source_metadata_modified": "",
            
172
  "state": "active",
172
  "state": "active",
            
173
  "subject_areas": [
173
  "subject_areas": [
            
174
    {
174
    {
            
175
      "subject_area_additional": "",
175
      "subject_area_additional": "",
            
176
      "subject_area_name": "Computer Science"
176
      "subject_area_name": "Computer Science"
            
177
    }
177
    }
            
178
  ],
178
  ],
            
179
  "tags": [],
179
  "tags": [],
            
180
  "title": "Evaluated artifact for \"quantifying software reliability 
180
  "title": "Evaluated artifact for \"quantifying software reliability 
            
181
via model-counting\"",
181
via model-counting\"",
            
182
  "type": "vdataset",
182
  "type": "vdataset",
            
183
  "url": "https://doi.org/10.35097/1520"
183
  "url": "https://doi.org/10.35097/1520"
            
184
}
184
}