Printing ARG info for earlier refinements in Predicate Abstraction SBE

[Artjom Plaunov]

Dear CPAchecker Team,

I am using CPAchecker Predicate analysis with SBE to analyze how predicate abstraction model checking works on some simple programs. I am using predicateAnalysis-PredAbsRefiner-SBE.properties, and I want to see what abstract states are being reached on each refinement step.

So I modified the analysis to set this: 

# Export one abstraction formula for each abstraction state into a file?
cpa.predicate.abstractions.export = true

I notice that the outputted abstractions.txt file has information for the latest refinement, as shown in ARG.dot, but there is no information for abstract states in earlier refinement steps, as shown in ARGRefinements.dot. 

I'm wondering if there's a config I can use for this. If not, I would be happy to contribute!

Best,

Artjom Plaunov

[Philipp Wendler]

Hi Artjom,

Am 19.08.23 um 01:26 schrieb Artjom Plaunov:

> I notice that the outputted abstractions.txt file has information for the
> latest refinement, as shown in ARG.dot, but there is no information for
> abstract states in earlier refinement steps, as shown in
> ARGRefinements.dot.
>
> I'm wondering if there's a config I can use for this. If not, I would be
> happy to contribute!

I don't think we have a usable export format for this.

In order to implement this, one would have to keep references to all
these abstractions, which is something that we normally don't do, and
which does not fit nicely into the way how CPAs and CEGAR work in
CPAchecker. It is certainly doable, though.

What would you like to do with these data? Are you just interested in
looking at them? Our log file might then be a good source of information.

Greetings
Philipp

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Artjom Plaunov]

Hi Philipp,

Thank you for getting back to me. I am just analyzing results; in particular I am running some simple programs in order to analyze how predicate abstraction explores the ARG on each refinement step, and what predicates are being introduced at which locations. 

For now I found a quick workaround for my own purposes, which was to limit the number of CEGAR iterations to k, and that way I can analyze the "abstractions.txt" file for the latest refinement step/exploration. 

I am wondering if the following config is also usable:

# Export abstraction formulas as (way more readable) expressions.
cpa.predicate.abstractions.asExpressions = true

I tried to add it to the predicate analysis config, but I could not see any results/change in output for the formulas. For now I am just reading off the SMT-lib2 formulas. 

Best,

Artjom Plaunov

[Philipp Wendler]

Hi Artjom,

Am 21.08.23 um 19:12 schrieb Artjom Plaunov:

> For now I found a quick workaround for my own purposes, which was to limit
> the number of CEGAR iterations to k, and that way I can analyze the
> "abstractions.txt" file for the latest refinement step/exploration.

Good idea!

> I am wondering if the following config is also usable:
>
> # Export abstraction formulas as (way more readable) expressions.
> cpa.predicate.abstractions.asExpressions = true

That option changes only the format of the abstractions.
You should no longer see SMTLib2 but an own expression syntax in
abstractions.txt.

[Artjom Plaunov]

Yes something like a basic expression syntax would be handy, however I get the following issue when I try to set the flag. 

To recreate the issue: I am running "predicateAnalysis-PredAbsRefiner-SBE" as the config, and to make my modifications I am editing the includes/predicateAnalysis.properties file, which is where I am setting the cpa.predicate.abstractions.asExpressions flag to true. 

Command: CPAchecker-2.2-unix/scripts/cpa.sh -config CPAchecker-2.2-unix/config/predicateAnalysis-PredAbsRefiner-SBE.properties -preprocess example.c

Output: The following configuration options were specified but are not used:

 cpa.predicate.abstractions.asExpressions
 (CPAchecker.printConfigurationWarnings, WARNING)

What may be stopping it from being used, even though it is specified? 

[Philipp Wendler]

Hi Artjom,

Am 23.08.23 um 01:35 schrieb Artjom Plaunov:

> To recreate the issue: I am running "predicateAnalysis-PredAbsRefiner-SBE"
> as the config, and to make my modifications I am editing the
> includes/predicateAnalysis.properties file, which is where I am setting the
> cpa.predicate.abstractions.asExpressions flag to true.

Side note:
I would not recommend to edit the supplied config files, I guess it is
easy to loose overview when doing so. Every config option can also be
specified on the command line with
-setprop foo=bar

> *Command:* CPAchecker-2.2-unix/scripts/cpa.sh -config
> CPAchecker-2.2-unix/config/predicateAnalysis-PredAbsRefiner-SBE.properties
> -preprocess example.c

Side note:
You can abbreviate the "-config ..." part with
-predicateAnalysis-PredAbsRefiner-SBE

> *Output: *The following configuration options were specified but are not

> used:
> cpa.predicate.abstractions.asExpressions
> (CPAchecker.printConfigurationWarnings, WARNING)
>
> What may be stopping it from being used, even though it is specified?

This config option was introduced only this year, so it is not yet
preset in CPAchecker 2.2.
You would need to use the current development version (either from the
Docker image or by compiling yourself with ant).

[Artjom Plaunov]

Hi Philipp, 

Thank you very much for the side notes and for the solution to my problem, I downloaded the development version and the config works on there. 

-Artjom