Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] What is the point of ``All models'' in Alt-Ergo?

 From Iguernlala Mohamed <mohamed.iguernlala at ocamlpro.com>:

======
Hi,

Le 27/01/2016 04:36, Wolfram Kahl a écrit :
 > Since I cannot find Alt-Ergo documentation nor mailing list,
 > I ask this question here, since I am using it only from Frama-C:

As said on Alt-Ergo's website (alt-ergo.ocamlpro.com), The issues
tracker is here: https://github.com/OCamlPro/alt-ergo/issues

 > What is the point of the ``All models'' option in Alt-Ergo?
As said with the help flag (alt-ergo -h), -all-models is experimental.
More precisely, it is a
one-day hack we made for an intern 5 years ago.

 > With that enabled (I am using it via the GUI as started from
 > WP-goals in Frama-C), it has no trouble to decide
 >
 >    //@ lemma falsum: 0 == 1;
 >
 > as ``Valid (0.01s)''.

Because, with this option enabled, every time Alt-Ergo finds a model, it
(is supposed to) (1) dump(s) it on standard output, and then (2)
act as if the branch was unsat to use backtracking capabilities of the
solver and search for other models.

So, it is easy to detect (when the option is activated) whether the
input formula is unsat (valid) or not by updating a global flag when the
first model is found. Unfortunately, this was not done during the
one-day hack .... and no one complained about this behavior. :-)

 > (Without that option, it only says ``I don't know (sat) (0.01s)'',
 > which I still consider as a rather weak answer...)

Current versions of Alt-Ergo never try to investigate whether the input
formula is invalid (sat) when they fail to prove it is valid(unsat),
even on trivial formulas like "0 = 1"

 > The closest I found to documentation is the help flag:
 >
 >    alt-ergo -h
 >
 > produces
 >
 >    -all-models experimental support for all models
 >    -model experimental support for models on labeled terms
 >    -complete-model experimental support for complete model
 >
 > , but I don't quite know how I am supposed to understand these ---
 > is validity of falsum a result of the experimental nature of these,
 > or is it by design of ``all models''?

By design of "all models" as said above, but it could be fixed. A
workaround is to run Alt-Ergo twice on the Formula: once without the
option to see if the forumula is valid, and once with the option to get
models.

Regards,
Mohamed.

-- 
Senior R&D Engineer, OCamlPro SAS
Research Associate, VALS team, LRI
Webpage: http://www.iguer.info