Commit e0b6c42c authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

modified timeout to 1 min

parent 646d9c0e
......@@ -119,7 +119,7 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
\smallskip
\mypar{Experiments.}
We run \cspenp over the four benchmark suites, using a Ubuntu-16.04 64-bit lap-top with an Intel Core i5-8250U CPU and 2GB RAM.
The experimental results are summarized in Table~\ref{tab-exp}. We set the timeout to 30 seconds. The statistics of average time and maximum time do not include the time of timeout instances.
The experimental results are summarized in Table~\ref{tab-exp}. We set the timeout to 60 seconds. The statistics of average time and maximum time do not include the time of timeout instances.
To the best of our knowledge, there have not been solvers that are capable of solving the \slah\ formulas that include, points-to, block, and $\hls{}$ atoms.
The solver SLar~\cite{KimuraT17} was designed to solve entailment problems involving points-to, block, and $\ls{}$ atoms. Nevertheless, we are unable to find a way to access SLar, thus failing to compare with it on ASL formulas.
Moreover, the examples used by SLar, available online, are in a format that seems nontrivial to translate into the SL-COMP format.
......@@ -149,9 +149,9 @@ To the best of our knowledge, there have not been solvers that are capable of so
\hline
MEM-ENT & 43 & 0 & 3.05 & 0.34 & 9.98 \\
\hline
RANDOM-ENT & 59 & 7 & 6.66 & 0.04 & 29.57 \\
RANDOM-ENT & 59 & 2 & 13.39 & 0.04 & 48.85 \\
\hline
TOTAL & 102 & 7 & 5.02 & 0.04 & 29.57 \\
TOTAL & 102 & 2 & 8.94 & 0.04 & 48.85 \\
\hline
\end{tabular}
\end{center}
......@@ -168,7 +168,7 @@ namely MEM-SAT and MEM-ENT, with the average time in 0.05 and 3.05 seconds respe
Table~\ref{tab-exp} shows that some entailment instances
are challenging for \cspenp. %\todo{speed if size increase}
For instance, the maximum time in MEM-ENT suite is
9.98, and there are 7 timeout instances in RANDOM-ENT suite (5 examples in less than 1 min, and 2 example in more than 2 min).
9.98, and there are 2 timeout instances in RANDOM-ENT suite (more than 2 min).
By inspecting these challenging instances, we found that
(i) they require splitting some spatial atoms ($\blk{}$ or $\hls{}$) in the antecedent,
which is potentially time-consuming, and
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment