Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / backends / Horn / horn_backend.ml @ 8d0c1f8e

History | View | Annotate | Download (2.43 KB)

# Date Author Comment
2ed9b6f2 01/07/2016 04:41 PM Pierre-Loïc Garoche

solved bug: missing parenthesis in enum typedef

5df5dd85 12/16/2015 03:18 PM Pierre-Loïc Garoche

Merge branch 'master' into horn_enum_types

Conflicts:
src/backends/Horn/horn_backend.ml

0dee2bc1 11/20/2015 06:41 PM Pierre-Loïc Garoche

Refactoring of the horn backend with Reset/Step instead of Init/Step.
Teme, please perform a string non regression test wrt the previous version, to make sure we have the same model checking results.

2580acfd 11/06/2015 06:09 PM Teme Kahsai

fixed a printing bug in horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@481 041b043f-8d7c-46b2-b46e-ef0dd855326e

50f7d587 10/09/2015 07:23 PM Pierre-Loïc Garoche

bug:double def fr init rules

7c95dcab 10/08/2015 07:11 PM Pierre-Loïc Garoche

Two fresh branches :)
to manage enum and arrays in the horn backend.

cdf01754 05/05/2015 07:30 PM Teme Kahsai

small logging change

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@455 041b043f-8d7c-46b2-b46e-ef0dd855326e

ad6b7375 05/05/2015 07:30 PM Teme Kahsai

small logging change

8deaa2dd 05/05/2015 01:17 AM Teme Kahsai

do not use lusi for horn, and some logging for horn

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@451 041b043f-8d7c-46b2-b46e-ef0dd855326e

9c4624e4 05/05/2015 01:17 AM Teme Kahsai

do not use lusi for horn, and some logging for horn

c89faaa4 03/24/2015 09:54 PM Teme Kahsai

synch with svn

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@429 041b043f-8d7c-46b2-b46e-ef0dd855326e

933ee7a3 03/24/2015 09:54 PM Teme Kahsai

synch with svn

3a87efb8 03/24/2015 09:54 PM Teme Kahsai

fixing double printing of horn rules

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@428 041b043f-8d7c-46b2-b46e-ef0dd855326e

eec8ce11 03/24/2015 09:54 PM Teme Kahsai

fixing double printing of horn rules

228ebb2c 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@425 041b043f-8d7c-46b2-b46e-ef0dd855326e

9d01f989 03/17/2015 08:30 AM Pierre-Loïc Garoche

Print the types

922ed789 03/16/2015 08:31 PM Teme Kahsai

mapping horn values to lustre values in xml format

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@423 041b043f-8d7c-46b2-b46e-ef0dd855326e

720f159a 03/16/2015 08:31 PM Teme Kahsai

mapping horn values to lustre values in xml format

b701409d 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@422 041b043f-8d7c-46b2-b46e-ef0dd855326e

96d33ff2 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

193a5ca6 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@421 041b043f-8d7c-46b2-b46e-ef0dd855326e

97d3f81a 03/16/2015 08:31 PM Teme Kahsai

sync horn backend

99d9ac94 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@419 041b043f-8d7c-46b2-b46e-ef0dd855326e

24a55d0d 03/16/2015 08:30 PM Teme Kahsai

fixing double printing of horn rules

c7c6ef4c 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@417 041b043f-8d7c-46b2-b46e-ef0dd855326e

62f65f02 03/16/2015 08:30 PM Teme Kahsai

Fixed conflict with the svn trunk version

3ca6d126 03/05/2015 11:48 PM Pierre-Loïc Garoche

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@414 041b043f-8d7c-46b2-b46e-ef0dd855326e

e9c64a30 03/05/2015 11:48 PM Pierre-Loïc Garoche

Reactivated the generation of traceability information
Changed the test-compile to use the horn-traces and the horn-queries option

7d9df109 03/03/2015 09:10 PM Teme Kahsai

added invariants

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@412 041b043f-8d7c-46b2-b46e-ef0dd855326e

f133f964 03/03/2015 09:10 PM Teme Kahsai

added invariants

8d4fddd8 03/03/2015 09:10 PM Teme Kahsai

including invariants

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@411 041b043f-8d7c-46b2-b46e-ef0dd855326e

ea94d58f 03/03/2015 09:10 PM Teme Kahsai

including invariants

5cf953ec 03/03/2015 09:10 PM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@410 041b043f-8d7c-46b2-b46e-ef0dd855326e

3c862628 03/03/2015 09:10 PM Teme Kahsai

Fixed horn backend to make query for properties. More work needed for cex

a2d97a3e 07/09/2014 09:57 AM Pierre-Loïc Garoche

Updated the licence info and header for each file.
Moved backends in separate folders

git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e

b38ffff3 07/09/2014 09:57 AM Pierre-Loïc Garoche

Updated the licence info and header for each file.
Moved backends in separate folders