From aa6a0db9b38cde04c8d7111a1e7a65f3c3bb901d Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Thu, 2 Jan 2025 13:28:01 +0100 Subject: [PATCH 01/49] refactored example structure --- pgfexamples/README.md | 17 ++++++++++------- pgfexamples/equivalence/loop_free/.gitkeep | 0 .../equivalence/loop_free/invariants/.gitkeep | 0 .../loopy}/17_die_even.pgcl | 0 .../loopy}/bit_flip_conditioning.pgcl | 0 .../loopy}/condand.pgcl | 0 .../loopy}/dep_bern.pgcl | 0 .../loopy}/endless_conditioning.pgcl | 0 .../loopy}/geometric.pgcl | 0 .../loopy}/geometric_observe.pgcl | 0 .../loopy}/geometric_observe_invariant.pgcl | 0 .../loopy}/geometric_shifted.pgcl | 0 .../invariants/17_die_even_invariant.pgcl | 0 .../bit_flip_conditioning_invariant.pgcl | 0 .../loopy}/invariants/condand_invariant.pgcl | 0 .../loopy}/invariants/dep_bern_invariant.pgcl | 0 .../endless_conditioning_invariant.pgcl | 0 .../loopy}/invariants/geometric_invariant.pgcl | 0 .../invariants/geometric_shifted_invariant.pgcl | 0 .../loopy}/invariants/ky_die_2_invariant.pgcl | 0 .../loopy}/invariants/ky_die_invariant.pgcl | 0 .../invariants/n_geometric_invariant.pgcl | 0 .../invariants/nested_while_inv_inner.pgcl | 0 .../invariants/nested_while_inv_outer.pgcl | 0 .../invariants/random_walk_invariant.pgcl | 0 .../rejection_sampling_invariant.pgcl | 0 .../running_paper_example_invariant.pgcl | 0 .../invariants/sequential_loops_first_inv.pgcl | 0 .../invariants/sequential_loops_second_inv.pgcl | 0 .../skip_rejection_sampling_invariant.pgcl | 0 .../invariants/trivial_iid_invariant.pgcl | 0 .../loopy}/ky_die.pgcl | 0 .../loopy}/ky_die_2.pgcl | 0 .../loopy}/n_geometric.pgcl | 0 .../loopy}/nested_while.pgcl | 0 .../loopy}/random_walk.pgcl | 0 .../loopy}/running_paper_example.pgcl | 0 .../loopy}/sequential_loops.pgcl | 0 .../loopy}/skip_rejection_sampling.pgcl | 0 .../loopy}/trivial_iid.pgcl | 0 .../cond_and.pgcl | 0 .../fast_dice_roller.pgcl | 0 .../faulty_decrement.pgcl | 0 .../geometric.pgcl | 0 .../geometric_counter.pgcl | 0 .../modulo_geometric.pgcl | 0 .../nontermination.pgcl | 0 .../random_walk.pgcl | 0 .../skip_random_walk_counter.pgcl | 0 .../skip_sequential_loops.pgcl | 0 .../subdist_enter.pgcl | 0 .../thirds_geometric.pgcl | 0 52 files changed, 10 insertions(+), 7 deletions(-) create mode 100644 pgfexamples/equivalence/loop_free/.gitkeep create mode 100644 pgfexamples/equivalence/loop_free/invariants/.gitkeep rename pgfexamples/{loop_equivalence => equivalence/loopy}/17_die_even.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/bit_flip_conditioning.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/condand.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/dep_bern.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/endless_conditioning.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/geometric.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/geometric_observe.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/geometric_observe_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/geometric_shifted.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/17_die_even_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/bit_flip_conditioning_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/condand_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/dep_bern_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/endless_conditioning_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/geometric_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/geometric_shifted_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/ky_die_2_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/ky_die_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/n_geometric_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/nested_while_inv_inner.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/nested_while_inv_outer.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/random_walk_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/rejection_sampling_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/running_paper_example_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/sequential_loops_first_inv.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/sequential_loops_second_inv.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/skip_rejection_sampling_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/invariants/trivial_iid_invariant.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/ky_die.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/ky_die_2.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/n_geometric.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/nested_while.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/random_walk.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/running_paper_example.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/sequential_loops.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/skip_rejection_sampling.pgcl (100%) rename pgfexamples/{loop_equivalence => equivalence/loopy}/trivial_iid.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/cond_and.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/fast_dice_roller.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/faulty_decrement.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/geometric.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/geometric_counter.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/modulo_geometric.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/nontermination.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/random_walk.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/skip_random_walk_counter.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/skip_sequential_loops.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/subdist_enter.pgcl (100%) rename pgfexamples/{evt_invariants => invariant_synthesis}/thirds_geometric.pgcl (100%) diff --git a/pgfexamples/README.md b/pgfexamples/README.md index 89d3aa9..86dfb50 100644 --- a/pgfexamples/README.md +++ b/pgfexamples/README.md @@ -7,17 +7,20 @@ pgfexamples/ ├── comparison # Comparisons with other tools / paradigms │   ├── ADDcomparison # Comparisons with Algebraic Decision Diagrams │   └── psicomparison # Comparisons with Psi -│   ├── inference +│   ├── inference │   └── psi_fails # Examples where Psi fails -├── evt_invariants # Synthesis of expected visiting time invariants -├── independence # Independent variables +├── equivalence # Equivalence of two programs +│   ├── loop_free # Programs without loops +│   └── invariants # ... and their counterparts +│   └── loopy # Programs with loops +│   └── invariants # ... and their loop-free counterpart +├── independence # Checks for independent variables ├── inference # Calculation of posterior distribution │   ├── loop_free # ... without while-loops │   │   └── conditioning # ... with observe-statements │   └── loopy # ... with while-loops │   └── conditioning # ... with observe-statements -├── loop_equivalence # Equality of loopy and loop-free programs -│   └── invariants # Corresponding loop-free programs +├── invariant_synthesis # Synthesis of (expected visiting time) invariants └── template_parameter_synthesis # Equality of loopy and loop-free programs with parameters -    └── invariants # Corresponding loop-free programs - ``` \ No newline at end of file + └── invariants # Corresponding loop-free programs +``` \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/.gitkeep b/pgfexamples/equivalence/loop_free/.gitkeep new file mode 100644 index 0000000..e69de29 diff --git a/pgfexamples/equivalence/loop_free/invariants/.gitkeep b/pgfexamples/equivalence/loop_free/invariants/.gitkeep new file mode 100644 index 0000000..e69de29 diff --git a/pgfexamples/loop_equivalence/17_die_even.pgcl b/pgfexamples/equivalence/loopy/17_die_even.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/17_die_even.pgcl rename to pgfexamples/equivalence/loopy/17_die_even.pgcl diff --git a/pgfexamples/loop_equivalence/bit_flip_conditioning.pgcl b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/bit_flip_conditioning.pgcl rename to pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl diff --git a/pgfexamples/loop_equivalence/condand.pgcl b/pgfexamples/equivalence/loopy/condand.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/condand.pgcl rename to pgfexamples/equivalence/loopy/condand.pgcl diff --git a/pgfexamples/loop_equivalence/dep_bern.pgcl b/pgfexamples/equivalence/loopy/dep_bern.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/dep_bern.pgcl rename to pgfexamples/equivalence/loopy/dep_bern.pgcl diff --git a/pgfexamples/loop_equivalence/endless_conditioning.pgcl b/pgfexamples/equivalence/loopy/endless_conditioning.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/endless_conditioning.pgcl rename to pgfexamples/equivalence/loopy/endless_conditioning.pgcl diff --git a/pgfexamples/loop_equivalence/geometric.pgcl b/pgfexamples/equivalence/loopy/geometric.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/geometric.pgcl rename to pgfexamples/equivalence/loopy/geometric.pgcl diff --git a/pgfexamples/loop_equivalence/geometric_observe.pgcl b/pgfexamples/equivalence/loopy/geometric_observe.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/geometric_observe.pgcl rename to pgfexamples/equivalence/loopy/geometric_observe.pgcl diff --git a/pgfexamples/loop_equivalence/geometric_observe_invariant.pgcl b/pgfexamples/equivalence/loopy/geometric_observe_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/geometric_observe_invariant.pgcl rename to pgfexamples/equivalence/loopy/geometric_observe_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/geometric_shifted.pgcl b/pgfexamples/equivalence/loopy/geometric_shifted.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/geometric_shifted.pgcl rename to pgfexamples/equivalence/loopy/geometric_shifted.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/17_die_even_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/17_die_even_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/bit_flip_conditioning_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/bit_flip_conditioning_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/condand_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/condand_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/dep_bern_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/dep_bern_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/endless_conditioning_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/endless_conditioning_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/geometric_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/geometric_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/geometric_shifted_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/geometric_shifted_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/ky_die_2_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/ky_die_2_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/ky_die_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/ky_die_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/n_geometric_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/n_geometric_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/nested_while_inv_inner.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/nested_while_inv_inner.pgcl rename to pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/nested_while_inv_outer.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/nested_while_inv_outer.pgcl rename to pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/random_walk_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/random_walk_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/rejection_sampling_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/rejection_sampling_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/running_paper_example_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/running_paper_example_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/sequential_loops_first_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/sequential_loops_first_inv.pgcl rename to pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/sequential_loops_second_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/sequential_loops_second_inv.pgcl rename to pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/skip_rejection_sampling_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/skip_rejection_sampling_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/invariants/trivial_iid_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/invariants/trivial_iid_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl diff --git a/pgfexamples/loop_equivalence/ky_die.pgcl b/pgfexamples/equivalence/loopy/ky_die.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/ky_die.pgcl rename to pgfexamples/equivalence/loopy/ky_die.pgcl diff --git a/pgfexamples/loop_equivalence/ky_die_2.pgcl b/pgfexamples/equivalence/loopy/ky_die_2.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/ky_die_2.pgcl rename to pgfexamples/equivalence/loopy/ky_die_2.pgcl diff --git a/pgfexamples/loop_equivalence/n_geometric.pgcl b/pgfexamples/equivalence/loopy/n_geometric.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/n_geometric.pgcl rename to pgfexamples/equivalence/loopy/n_geometric.pgcl diff --git a/pgfexamples/loop_equivalence/nested_while.pgcl b/pgfexamples/equivalence/loopy/nested_while.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/nested_while.pgcl rename to pgfexamples/equivalence/loopy/nested_while.pgcl diff --git a/pgfexamples/loop_equivalence/random_walk.pgcl b/pgfexamples/equivalence/loopy/random_walk.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/random_walk.pgcl rename to pgfexamples/equivalence/loopy/random_walk.pgcl diff --git a/pgfexamples/loop_equivalence/running_paper_example.pgcl b/pgfexamples/equivalence/loopy/running_paper_example.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/running_paper_example.pgcl rename to pgfexamples/equivalence/loopy/running_paper_example.pgcl diff --git a/pgfexamples/loop_equivalence/sequential_loops.pgcl b/pgfexamples/equivalence/loopy/sequential_loops.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/sequential_loops.pgcl rename to pgfexamples/equivalence/loopy/sequential_loops.pgcl diff --git a/pgfexamples/loop_equivalence/skip_rejection_sampling.pgcl b/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/skip_rejection_sampling.pgcl rename to pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl diff --git a/pgfexamples/loop_equivalence/trivial_iid.pgcl b/pgfexamples/equivalence/loopy/trivial_iid.pgcl similarity index 100% rename from pgfexamples/loop_equivalence/trivial_iid.pgcl rename to pgfexamples/equivalence/loopy/trivial_iid.pgcl diff --git a/pgfexamples/evt_invariants/cond_and.pgcl b/pgfexamples/invariant_synthesis/cond_and.pgcl similarity index 100% rename from pgfexamples/evt_invariants/cond_and.pgcl rename to pgfexamples/invariant_synthesis/cond_and.pgcl diff --git a/pgfexamples/evt_invariants/fast_dice_roller.pgcl b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl similarity index 100% rename from pgfexamples/evt_invariants/fast_dice_roller.pgcl rename to pgfexamples/invariant_synthesis/fast_dice_roller.pgcl diff --git a/pgfexamples/evt_invariants/faulty_decrement.pgcl b/pgfexamples/invariant_synthesis/faulty_decrement.pgcl similarity index 100% rename from pgfexamples/evt_invariants/faulty_decrement.pgcl rename to pgfexamples/invariant_synthesis/faulty_decrement.pgcl diff --git a/pgfexamples/evt_invariants/geometric.pgcl b/pgfexamples/invariant_synthesis/geometric.pgcl similarity index 100% rename from pgfexamples/evt_invariants/geometric.pgcl rename to pgfexamples/invariant_synthesis/geometric.pgcl diff --git a/pgfexamples/evt_invariants/geometric_counter.pgcl b/pgfexamples/invariant_synthesis/geometric_counter.pgcl similarity index 100% rename from pgfexamples/evt_invariants/geometric_counter.pgcl rename to pgfexamples/invariant_synthesis/geometric_counter.pgcl diff --git a/pgfexamples/evt_invariants/modulo_geometric.pgcl b/pgfexamples/invariant_synthesis/modulo_geometric.pgcl similarity index 100% rename from pgfexamples/evt_invariants/modulo_geometric.pgcl rename to pgfexamples/invariant_synthesis/modulo_geometric.pgcl diff --git a/pgfexamples/evt_invariants/nontermination.pgcl b/pgfexamples/invariant_synthesis/nontermination.pgcl similarity index 100% rename from pgfexamples/evt_invariants/nontermination.pgcl rename to pgfexamples/invariant_synthesis/nontermination.pgcl diff --git a/pgfexamples/evt_invariants/random_walk.pgcl b/pgfexamples/invariant_synthesis/random_walk.pgcl similarity index 100% rename from pgfexamples/evt_invariants/random_walk.pgcl rename to pgfexamples/invariant_synthesis/random_walk.pgcl diff --git a/pgfexamples/evt_invariants/skip_random_walk_counter.pgcl b/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl similarity index 100% rename from pgfexamples/evt_invariants/skip_random_walk_counter.pgcl rename to pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl diff --git a/pgfexamples/evt_invariants/skip_sequential_loops.pgcl b/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl similarity index 100% rename from pgfexamples/evt_invariants/skip_sequential_loops.pgcl rename to pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl diff --git a/pgfexamples/evt_invariants/subdist_enter.pgcl b/pgfexamples/invariant_synthesis/subdist_enter.pgcl similarity index 100% rename from pgfexamples/evt_invariants/subdist_enter.pgcl rename to pgfexamples/invariant_synthesis/subdist_enter.pgcl diff --git a/pgfexamples/evt_invariants/thirds_geometric.pgcl b/pgfexamples/invariant_synthesis/thirds_geometric.pgcl similarity index 100% rename from pgfexamples/evt_invariants/thirds_geometric.pgcl rename to pgfexamples/invariant_synthesis/thirds_geometric.pgcl From 138c61f979aa1a266f5c6efeb3b45e9663969f20 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sat, 11 Jan 2025 13:15:33 +0100 Subject: [PATCH 02/49] adjusted benchmark script to execute files with provided commands --- benchmark_comparison.py | 320 ++++++++++++------ .../equivalence/loopy/17_die_even.pgcl | 1 + .../loopy/bit_flip_conditioning.pgcl | 1 + pgfexamples/equivalence/loopy/condand.pgcl | 1 + pgfexamples/equivalence/loopy/dep_bern.pgcl | 1 + .../loopy/endless_conditioning.pgcl | 2 +- pgfexamples/equivalence/loopy/geometric.pgcl | 1 + .../equivalence/loopy/geometric_observe.pgcl | 1 + .../equivalence/loopy/geometric_shifted.pgcl | 1 + .../invariants/17_die_even_invariant.pgcl | 1 + .../bit_flip_conditioning_invariant.pgcl | 1 + .../loopy/invariants/condand_invariant.pgcl | 1 + .../loopy/invariants/dep_bern_invariant.pgcl | 1 + .../endless_conditioning_invariant.pgcl | 1 + .../loopy/invariants/geometric_invariant.pgcl | 1 + .../geometric_observe_invariant.pgcl | 1 + .../geometric_shifted_invariant.pgcl | 1 + .../loopy/invariants/ky_die_2_invariant.pgcl | 1 + .../loopy/invariants/ky_die_invariant.pgcl | 1 + .../invariants/n_geometric_invariant.pgcl | 1 + .../invariants/nested_while_inv_inner.pgcl | 1 + .../invariants/nested_while_inv_outer.pgcl | 1 + .../invariants/random_walk_invariant.pgcl | 1 + .../rejection_sampling_invariant.pgcl | 1 + .../running_paper_example_invariant.pgcl | 1 + .../sequential_loops_first_inv.pgcl | 1 + .../sequential_loops_second_inv.pgcl | 1 + .../skip_rejection_sampling_invariant.pgcl | 1 + .../invariants/trivial_iid_invariant.pgcl | 1 + pgfexamples/equivalence/loopy/ky_die.pgcl | 1 + pgfexamples/equivalence/loopy/ky_die_2.pgcl | 1 + .../equivalence/loopy/n_geometric.pgcl | 1 + .../equivalence/loopy/nested_while.pgcl | 2 + .../equivalence/loopy/random_walk.pgcl | 1 + .../loopy/running_paper_example.pgcl | 1 + .../equivalence/loopy/sequential_loops.pgcl | 3 + .../loopy/skip_rejection_sampling.pgcl | 1 + .../equivalence/loopy/trivial_iid.pgcl | 1 + .../independence/infinite_multiplication.pgcl | 2 + .../independence/oblivious_transfer.pgcl | 1 + .../private_information_retriveal.pgcl | 1 + .../loop_free/conditioning/burgler_alarm.pgcl | 1 + .../loop_free/conditioning/caesar.pgcl | 1 + .../conditioning/conditioning_divergence.pgcl | 1 + .../conditioning/digitRecognition.pgcl | 1 + .../loop_free/conditioning/evidence1.pgcl | 1 + .../loop_free/conditioning/evidence2.pgcl | 1 + .../loop_free/conditioning/grass.pgcl | 1 + .../conditioning/infer_geom_mix.pgcl | 1 + .../conditioning/lin_regression_unbiased.pgcl | 1 + .../loop_free/conditioning/lucky_throw.pgcl | 1 + .../conditioning/monty_hall_nested.pgcl | 1 + .../conditioning/murder_mystery.pgcl | 1 + .../skip_lin_regression_biased.pgcl | 1 + .../conditioning/telephone_operator.pgcl | 1 + .../loop_free/conditioning/twocoins.pgcl | 1 + .../conditioning/undefined_normalization.pgcl | 1 + .../inference/loop_free/dnd_handicap.pgcl | 1 + pgfexamples/inference/loop_free/function.pgcl | 1 + pgfexamples/inference/loop_free/fuzzy_or.pgcl | 1 + pgfexamples/inference/loop_free/max.pgcl | 1 + .../inference/loop_free/monty_hall.pgcl | 1 + pgfexamples/inference/loop_free/pi.pgcl | 1 + pgfexamples/inference/loop_free/piranha.pgcl | 1 + .../inference/loop_free/poor_scale.pgcl | 1 + .../inference/loop_free/prob_collatz.pgcl | 1 + .../inference/loop_free/scalability.pgcl | 1 + .../loopy/conditioning/dep_bern.pgcl | 1 + .../loopy/conditioning/trivial_iid.pgcl | 1 + .../inference/loopy/dueling_cowboys.pgcl | 1 + .../inference/loopy/skip_exceeding_sum.pgcl | 1 + .../inference/loopy/skip_geom_dist.pgcl | 1 + .../inference/loopy/skip_random_walk.pgcl | 1 + .../inference/loopy/uniform_sampling.pgcl | 3 +- pgfexamples/invariant_synthesis/cond_and.pgcl | 1 + .../invariant_synthesis/fast_dice_roller.pgcl | 1 + .../invariant_synthesis/faulty_decrement.pgcl | 1 + .../invariant_synthesis/geometric.pgcl | 1 + .../geometric_counter.pgcl | 1 + .../invariant_synthesis/modulo_geometric.pgcl | 1 + .../invariant_synthesis/nontermination.pgcl | 1 + .../invariant_synthesis/random_walk.pgcl | 1 + .../skip_random_walk_counter.pgcl | 1 + .../skip_sequential_loops.pgcl | 1 + .../invariant_synthesis/subdist_enter.pgcl | 1 + .../invariant_synthesis/thirds_geometric.pgcl | 1 + ...ip_conditioning_generalized_parameter.pgcl | 1 + .../bit_flip_conditioning_parameter.pgcl | 1 + .../brp_obs_parameter.pgcl | 1 + .../dueling_cowboys_parameter.pgcl | 1 + .../geometric_observe_parameter.pgcl | 1 + .../geometric_parameter.pgcl | 1 + ...oning_generalized_parameter_invariant.pgcl | 1 + ...flip_conditioning_parameter_invariant.pgcl | 1 + .../brp_obs_parameter_invariant.pgcl | 1 + .../dueling_cowboys_parameter_invariant.pgcl | 1 + ...geometric_observe_parameter_invariant.pgcl | 1 + .../geometric_parameter_invariant.pgcl | 1 + .../ky_die_parameter_invariant.pgcl | 1 + .../n_geometric_parameter_invariant.pgcl | 1 + ...negative_binomial_parameter_invariant.pgcl | 1 + ...binomial_reversed_parameter_invariant.pgcl | 1 + .../random_walk_parameter_invariant.pgcl | 1 + .../ky_die_parameter.pgcl | 1 + .../n_geometric_parameter.pgcl | 1 + .../negative_binomial_parameter.pgcl | 1 + .../negative_binomial_reversed_parameter.pgcl | 1 + .../random_walk_parameter.pgcl | 1 + .../telephone_operator_parameter.pgcl | 3 + 109 files changed, 336 insertions(+), 101 deletions(-) rename pgfexamples/equivalence/loopy/{ => invariants}/geometric_observe_invariant.pgcl (95%) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 7082e5a..1a1361c 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -5,7 +5,7 @@ import sympy as sp import os from glob import glob - +import re # All files in the pgfexamples folder all_files: list[str] = [y for x in os.walk("pgfexamples") for y in glob(os.path.join(x[0], '*.pgcl'))] + [ @@ -13,21 +13,30 @@ # Timeouts / Exception runs # If files are not present, an empty list is returned -timeouts: list[str] = list(map(str.strip, open("timeouts.txt", "r").readlines())) \ +skip_files: list[str] = list(map(str.strip, open("timeouts.txt", "r").readlines())) \ if os.path.isfile("timeouts.txt") else [] + \ - list(map(str.strip, open("exceptions.txt", "r").readlines())) if os.path.isfile("exceptions.txt") else [] + list(map(str.strip, + open("exceptions.txt", "r").readlines())) if os.path.isfile( + "exceptions.txt") else [] # All available engines # (will be executed in this order) -engines = [ +engines: list[str] = [ "ginac", "symengine", "sympy" ] +# Default CLI args for files that do not contain any additional information +default_instruction: list[str] = ["main"] + +# https://stackoverflow.com/a/14693789 +ansi_escape = re.compile(r'\x1B(?:[@-Z\\-_]|\[[0-?]*[ -/]*[@-~])') + class Run: """ Represents a single run of one engine on one file. """ + def __init__(self, time, output, file): """ Initializes the Run object. @@ -60,6 +69,7 @@ class Configuration: """ Represents the configuration given by the user """ + def __init__(self, args): """ Initializes the Configuration object. @@ -123,7 +133,7 @@ def create_parser() -> argparse.ArgumentParser: "--engine", metavar="ENGINE", help="The engine that should be tested primarily. Separate multiple engines by ','. " + - "If unset, all engines are tested. Note: Engines will be executed in the order given. "+ + "If unset, all engines are tested. Note: Engines will be executed in the order given. " + f"Supported engines: {', '.join(engines)}." ) @@ -210,42 +220,55 @@ def benchmark(config: Configuration): # If output is wanted, set up the corresponding file if config.output_file is not None: - setup_outfile(config.output_file) + setup_outfile(config.output_file, config.engine) counter = 0 # For each file, test all engines for file in config.files: counter += 1 print(f"Now testing: {file} ({counter}/{len(config.files)})") - # Check if the current file is in timeouts - if file in timeouts and config.skip_timeouts: - print(f"File is in timeouts, skipping...") + if file in skip_files and config.skip_timeouts: + print(f"File is in skipped files, skipping...") continue engine_counter = 0 + + instructions = obtain_instructions(file) + skipped = False # For each engine, run the program for engine in config.engine: + if skipped: + continue + engine_counter += 1 print(f"Running {engine} ({engine_counter}/{len(config.engine)})") # Check if current file is in timeouts # Files can be added dynamically, hence the second check - if file in timeouts and config.skip_timeouts: - print(f"File is in timeouts, skipping...") + if file in skip_files and config.skip_timeouts: + print(f"File is in skipped files, skipping...") + skipped = True continue output = "" + + # Check if file is to be skipped + if not instructions: + print("File marked to be skipped...") + skipped = True + continue # Execute the program + + cmd = ["python", "prodigy/cli.py", "--engine", engine, *instructions] try: - cmd = ["python", "prodigy/cli.py", "--engine", engine, "main", file] output = subprocess.check_output(cmd, timeout=config.timeout).decode() - print(output) except TimeoutExpired as e: # Command timed out with open("timeouts.txt", "a") as f: # Write the file in "timeouts.txt" and add to the list f.write(file + "\n") - timeouts.append(file) + skip_files.append(file) + skipped = True if config.fail_on_error: raise e continue @@ -254,7 +277,8 @@ def benchmark(config: Configuration): with open("exceptions.txt", "a") as f: # Write the file in "timeouts.txt" and add to the list f.write(file + "\n") - timeouts.append(file) + skip_files.append(file) + skipped = True if config.fail_on_error: raise e continue @@ -263,121 +287,218 @@ def benchmark(config: Configuration): raise RuntimeError("No output was captured.") # Parse output + print(output) output = output.splitlines() + run = capture_output(output, instructions, file) + print(run) - # Sometimes other stuff is logged, which is captured - # but not interesting for the analysis. - # The interesting part begins with "Result: [...]" - while "Result" not in output[0]: - output = output[1:] - - # Add time to the dictionary - times[engine].append( - Run( - time=float(output[-1].split()[-2]), - output=tuple( - str( - output[0] - .split("\x1b")[2] - .split("[92m")[1] - ).removeprefix("(") - .removesuffix(")") - .split(",") - ), # Very hacky lol - file=file - ) - ) + # Add the result to the dictionary + times[engine].append(run) + fail = False # Compare results if at least two engines are selected and file wasn't skipped once (if skip_timeouts is set) - if len(config.engine) > 1 and (not config.skip_timeouts or file not in timeouts): - try: - results: dict[str, list[sp.Expr]] = {} - for engine in config.engine: - # Results for "engine" look like this: - # expr, error_prob - results[engine] = [sp.S(times[engine][-1].output[i]) for i in range(2)] - except Exception as e: - # Something went wrong while parsing - print(str(e)) - if config.fail_on_error: - raise e - continue - - fail = False - # Compare all results - for engine in config.engine: - if fail: - break - # Engines the current engine is compared against - # Technically, we only need one direction of equality - # but this is more convenient - other_engines = set(results.keys()) - {engine} - for other_engine in other_engines: - if fail: - break - # Compare expr and error_prob - for i in range(2): - if fail: - break - try: - assert results[engine][i].equals(results[other_engine][i]), \ - f""" - Engine {engine} disagrees with engine {other_engine} on file {file}. - """ + "\n".join(f"{e}: {results[e][i]}" for e in engines) - except AssertionError as e: - with open("exceptions.txt", "a") as f: - # Write file to exception file - # We do not need to add file to timeouts, - # as the file was already checked - f.write(file + "\n") - print(str(e)) - if config.fail_on_error: - raise e - fail = True - break - - # Results are equal, add run to output file (if set) - if config.output_file is not None and not fail: - with open(config.output_file, "a") as f: - f.write(file) - for engine in config.engine: - f.write(f",{times[engine][-1].time}") - f.write("\n") - + if len(config.engine) > 1 and not skipped: + fail = compare_output({engine: times[engine][-1] for engine in config.engine}, instructions, file, config.fail_on_error) if not fail: print("Results are equal, continuing...") + # Write results if output file is set (and results are equal or just one engine is tested) + if config.output_file is not None and not fail and not skipped: + with open(config.output_file, "a") as f: + f.write(file) + for engine in config.engine: + f.write(f",{times[engine][-1].time}") + f.write("\n") # If generate markdown is set, create the Markdown table if config.generate_markdown: print("Generating markdown table...") generate_markdown_table(config.output_file, config.engine) -def setup_outfile(out_file: str): +def setup_outfile(out_file: str, engine_list: list[str]) -> None: # If file exists, rename it to filename_{i}.extension if os.path.isfile(out_file): i = 1 - new_name = out_file.split(".")[0] + f"_{i}." + out_file.split(".")[1] + new_name_template = lambda el: out_file.split(".")[0] + f"_{el}." + out_file.split(".")[1] + new_name = new_name_template(i) while os.path.isfile(new_name): i += 1 - new_name = out_file.split(".")[0] + f"_{i}." + out_file.split(".")[1] + new_name = new_name_template(i) os.rename(out_file, new_name) # Write header with open(out_file, "a") as f: f.write("file") - for engine in engines: + for engine in engine_list: f.write(f",{engine}") f.write("\n") -def generate_markdown_table(csv_file: str, engine_list: list[str]): +def obtain_instructions(file_path: str) -> list[str]: + """ + Reads the first line of given file and checks whether it is instructions for the command + """ + + with open(file_path, "r") as f: + first_line = f.readlines()[0] + + if first_line.startswith("#"): + # First line is an instruction + parts = list(map(str.strip, first_line.split()[1:])) + if parts == ["skip"]: + return [] + return parts + else: + # No instruction is given -> return the default instruction + print(f"No instruction found for {file_path}, executing default instruction...") + return default_instruction + [file_path] + + +def capture_output(output: list[str], cmd: list[str], file: str) -> Run: + # Remove ANSI + output = [ansi_escape.sub("", o) for o in output] + if "main" in cmd: + # Sometimes other stuff is logged, which is captured + # but not interesting for the analysis. + # The interesting part begins with "Result: [...]" + while "Result" not in output[0]: + output = output[1:] + return Run( + time=float(output[-1].split()[-2]), + output=tuple( + str(output[0].split("\t")[1]) + .removeprefix("(") + .removesuffix(")") + .split(",") + ), + file=file + ) + elif "check_equality" in cmd: + # TODO check parameter for parameter synthesis? + while "equivalent" not in output[0]: + output = output[1:] + return Run( + time=float(output[-1].split()[-2]), + output=(output[0].startswith("Program is equivalent to invariant")), + file=file + ) + elif "invariant_synthesis" in cmd: + while "Invariant: " not in output[0]: + output = output[1:] + return Run( + time=float(output[-1].split()[-2]), + output=output[0].split()[1], + file=file + ) + else: + # todo other methods + pass + + +def compare_output(outputs: dict[str, Run], cmd: list[str], file: str, fail_on_error: bool) -> bool: + fail = False + if "main" in cmd: + parsed_results: dict[str, tuple[sp.Expr, sp.Expr]] = {} + for engine in outputs.keys(): + try: + parsed_results[engine] = (sp.S(outputs[engine].output[0]), sp.S(outputs[engine].output[0])) + except Exception as e: + print(str(e)) + if fail_on_error: + raise e + + for engine in outputs.keys(): + other_engines = set(outputs.keys()) - {engine} + for other_engine in other_engines: + if fail: + break + for i in range(2): + if fail: + break + try: + assert parsed_results[engine][i].equals(parsed_results[other_engine][i]), \ + f""" + Engine {engine} disagrees with {other_engine} on file {file}. + """ + "\n".join(f"{e}: {parsed_results[e][i]}" for e in engines) + except AssertionError as e: + fail = True + with open("exceptions.txt", "a") as f: + # Write file to exception file + # We do not need to add file to timeouts, + # as the file was already checked + f.write(file + "\n") + print(str(e)) + if fail_on_error: + raise e + break + elif "equivalence" in cmd: + for engine in outputs.keys(): + other_engines = set(outputs.keys()) - {engine} + for other_engine in other_engines: + if fail: + break + try: + assert outputs[engine].output == outputs[other_engine].output, \ + f""" + Engine {engine} disagrees with {other_engine} on file {file}. + """ + "\n".join(f"{e}: {outputs[e].output}" for e in engines) + except AssertionError as e: + fail = True + with open("exceptions.txt", "a") as f: + # Write file to exception file + # We do not need to add file to timeouts, + # as the file was already checked + f.write(file + "\n") + print(str(e)) + if fail_on_error: + raise e + break + elif "invariant_synthesis" in cmd: + parsed_results: dict[str, sp.Expr] = {} + for engine in outputs.keys(): + try: + parsed_results[engine] = sp.S(outputs[engine].output) + except Exception as e: + print(str(e)) + if fail_on_error: + raise e + for engine in outputs.keys(): + other_engines = set(outputs.keys()) - {engine} + for other_engine in other_engines: + if fail: + break + try: + assert parsed_results[engine].equals(parsed_results[other_engine]), \ + f""" + Engine {engine} disagrees with {other_engine} on file {file}. + """ + "\n".join(f"{e}: {parsed_results[e]}" for e in engines) + except AssertionError as e: + fail = True + with open("exceptions.txt", "a") as f: + # Write file to exception file + # We do not need to add file to timeouts, + # as the file was already checked + f.write(file + "\n") + print(str(e)) + if fail_on_error: + raise e + break + else: + # TODO other methods + pass + return fail + + +def generate_markdown_table(csv_file: str, engine_list: list[str]) -> None: """ - Parses a given csv file to a Markdown table while highlighting the fastest result + Parses a given csv file to a Markdown table while highlighting the fastest result. :param csv_file: The csv file to be parsed. :param engine_list: A list of engines to be compared. """ + + # TODO should number of skipped runs be logged? + out_file = csv_file.split(".")[0] + "_format.md" # Read the output file @@ -416,7 +537,8 @@ def generate_markdown_table(csv_file: str, engine_list: list[str]): # Write the run f.write("|" + "|".join(line) + "|\n") # Write the average and summary - f.write("|Average|" + "|".join([f"{sum(results[i]) / len(results[i])}" for i in range(len(engine_list))]) + "|\n") + f.write( + "|Average|" + "|".join([f"{sum(results[i]) / len(results[i])}" for i in range(len(engine_list))]) + "|\n") f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n") diff --git a/pgfexamples/equivalence/loopy/17_die_even.pgcl b/pgfexamples/equivalence/loopy/17_die_even.pgcl index 7a60dc3..490a299 100644 --- a/pgfexamples/equivalence/loopy/17_die_even.pgcl +++ b/pgfexamples/equivalence/loopy/17_die_even.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/17_die_even.pgcl pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl nat c nat x nat temp diff --git a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl index 784f9f1..b2eacfb 100644 --- a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl +++ b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl bool b1 bool b2 bool b3 diff --git a/pgfexamples/equivalence/loopy/condand.pgcl b/pgfexamples/equivalence/loopy/condand.pgcl index f6cadad..357a340 100644 --- a/pgfexamples/equivalence/loopy/condand.pgcl +++ b/pgfexamples/equivalence/loopy/condand.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/condard.pgcl pgfexamples/equivalence/loopy/invariants/condard_invariant.pgcl nat n; nat m; diff --git a/pgfexamples/equivalence/loopy/dep_bern.pgcl b/pgfexamples/equivalence/loopy/dep_bern.pgcl index d6bdac7..445675a 100644 --- a/pgfexamples/equivalence/loopy/dep_bern.pgcl +++ b/pgfexamples/equivalence/loopy/dep_bern.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/dep_bern.pgcl pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl nat c; nat m; nat n; diff --git a/pgfexamples/equivalence/loopy/endless_conditioning.pgcl b/pgfexamples/equivalence/loopy/endless_conditioning.pgcl index eafd35a..2da03ce 100644 --- a/pgfexamples/equivalence/loopy/endless_conditioning.pgcl +++ b/pgfexamples/equivalence/loopy/endless_conditioning.pgcl @@ -1,4 +1,4 @@ - +# check_equality pgfexamples/equivalence/loopy/endless_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl nat x; while(x=1){ diff --git a/pgfexamples/equivalence/loopy/geometric.pgcl b/pgfexamples/equivalence/loopy/geometric.pgcl index 41346f6..a6f988e 100644 --- a/pgfexamples/equivalence/loopy/geometric.pgcl +++ b/pgfexamples/equivalence/loopy/geometric.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/geometric.pgcl pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl nat x; nat c; nat temp; diff --git a/pgfexamples/equivalence/loopy/geometric_observe.pgcl b/pgfexamples/equivalence/loopy/geometric_observe.pgcl index 00afd7f..053ad20 100644 --- a/pgfexamples/equivalence/loopy/geometric_observe.pgcl +++ b/pgfexamples/equivalence/loopy/geometric_observe.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/geometric_observe.pgcl pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl nat y; nat x; nat tmp; diff --git a/pgfexamples/equivalence/loopy/geometric_shifted.pgcl b/pgfexamples/equivalence/loopy/geometric_shifted.pgcl index a0b61ea..204bf33 100644 --- a/pgfexamples/equivalence/loopy/geometric_shifted.pgcl +++ b/pgfexamples/equivalence/loopy/geometric_shifted.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/geometric_shifted.pgcl pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl nat x; nat c; nat temp; diff --git a/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl index 6ccf4cf..0adcd7a 100644 --- a/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/17_die_even_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat c nat x nat temp diff --git a/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl index c3de1a9..f8e6abd 100644 --- a/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl @@ -1,3 +1,4 @@ +# skip bool b1 bool b2 bool b3 diff --git a/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl index a33c041..9e45b3a 100644 --- a/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/condand_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat n; nat m; diff --git a/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl index 353ff81..c82aa12 100644 --- a/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/dep_bern_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat c; nat m; nat n; diff --git a/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl index 67eab4a..4a2fbaa 100644 --- a/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/endless_conditioning_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat x; if (x = 1){ diff --git a/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl index 6f09ba7..5f5d0b1 100644 --- a/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/geometric_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; nat temp; diff --git a/pgfexamples/equivalence/loopy/geometric_observe_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl similarity index 95% rename from pgfexamples/equivalence/loopy/geometric_observe_invariant.pgcl rename to pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl index 26e3b0e..96c44b0 100644 --- a/pgfexamples/equivalence/loopy/geometric_observe_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/geometric_observe_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat y; nat x; nat tmp; diff --git a/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl index 68a360a..480ddc3 100644 --- a/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/geometric_shifted_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; nat temp; diff --git a/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl index 1af69cd..43fb190 100644 --- a/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat s; nat die; diff --git a/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl index 0c79de0..d20a42b 100644 --- a/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat s; nat die; diff --git a/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl index a17000b..3434b7f 100644 --- a/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat n; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl index 50b138c..7accc56 100644 --- a/pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat y; nat temp; diff --git a/pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl index 372d86c..c0a6001 100644 --- a/pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat y; nat c; diff --git a/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl index 3a5507f..0be24e5 100644 --- a/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat s; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl index 79baad0..bbbd817 100644 --- a/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/rejection_sampling_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat c; if(c%2=0){ diff --git a/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl index 72812bb..4b0d4b9 100644 --- a/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl index ca979cf..4dfada4 100644 --- a/pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl @@ -1,3 +1,4 @@ +# skip nat c; nat m; nat n; diff --git a/pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl index ecdf9ec..ce43346 100644 --- a/pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl @@ -1,3 +1,4 @@ +# skip nat m; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl index b699236..e604e82 100644 --- a/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/skip_rejection_sampling_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat c; if ( not (c%2=0)){ diff --git a/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl b/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl index 7abc1a1..c2cf3cd 100644 --- a/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl +++ b/pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat n; nat m; nat tmp; diff --git a/pgfexamples/equivalence/loopy/ky_die.pgcl b/pgfexamples/equivalence/loopy/ky_die.pgcl index b9e51c0..7e13989 100644 --- a/pgfexamples/equivalence/loopy/ky_die.pgcl +++ b/pgfexamples/equivalence/loopy/ky_die.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/ky_die.pgcl pgfexamples/equivalence/loopy/invariants/ky_die_invariant.pgcl nat s; nat die; diff --git a/pgfexamples/equivalence/loopy/ky_die_2.pgcl b/pgfexamples/equivalence/loopy/ky_die_2.pgcl index 90afe77..54f8d5b 100644 --- a/pgfexamples/equivalence/loopy/ky_die_2.pgcl +++ b/pgfexamples/equivalence/loopy/ky_die_2.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/ky_die_2.pgcl pgfexamples/equivalence/loopy/invariants/ky_die_2_invariant.pgcl nat s; nat die; diff --git a/pgfexamples/equivalence/loopy/n_geometric.pgcl b/pgfexamples/equivalence/loopy/n_geometric.pgcl index e1e29c9..c909730 100644 --- a/pgfexamples/equivalence/loopy/n_geometric.pgcl +++ b/pgfexamples/equivalence/loopy/n_geometric.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/n_geometric.pgcl pgfexamples/equivalence/loopy/invariants/n_geometric_invariant.pgcl nat n; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/nested_while.pgcl b/pgfexamples/equivalence/loopy/nested_while.pgcl index ae8b084..9835ce2 100644 --- a/pgfexamples/equivalence/loopy/nested_while.pgcl +++ b/pgfexamples/equivalence/loopy/nested_while.pgcl @@ -1,3 +1,5 @@ +# skip +# TODO how to do this with the CLI nat x; nat y; nat c; diff --git a/pgfexamples/equivalence/loopy/random_walk.pgcl b/pgfexamples/equivalence/loopy/random_walk.pgcl index f3533eb..266b329 100644 --- a/pgfexamples/equivalence/loopy/random_walk.pgcl +++ b/pgfexamples/equivalence/loopy/random_walk.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/random_walk.pgcl pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl nat s; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/running_paper_example.pgcl b/pgfexamples/equivalence/loopy/running_paper_example.pgcl index cd70bd6..d20607c 100644 --- a/pgfexamples/equivalence/loopy/running_paper_example.pgcl +++ b/pgfexamples/equivalence/loopy/running_paper_example.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/running_paper_example.pgcl pgfexamples/equivalence/loopy/invariants/running_paper_example_invariant.pgcl nat x; nat c; nat tmp; diff --git a/pgfexamples/equivalence/loopy/sequential_loops.pgcl b/pgfexamples/equivalence/loopy/sequential_loops.pgcl index d9136da..b2c3c00 100644 --- a/pgfexamples/equivalence/loopy/sequential_loops.pgcl +++ b/pgfexamples/equivalence/loopy/sequential_loops.pgcl @@ -1,3 +1,6 @@ +# skip +# TODO how to do this with CLI? +# check_equality pgfexamples/equivalence/loopy/sequential_loops.pgcl pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant.pgcl nat c; nat m; nat n; diff --git a/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl b/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl index fcd0e2c..8391271 100644 --- a/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl +++ b/pgfexamples/equivalence/loopy/skip_rejection_sampling.pgcl @@ -1,3 +1,4 @@ +# skip nat c; while (c%2=0){ diff --git a/pgfexamples/equivalence/loopy/trivial_iid.pgcl b/pgfexamples/equivalence/loopy/trivial_iid.pgcl index 7e4770b..871f817 100644 --- a/pgfexamples/equivalence/loopy/trivial_iid.pgcl +++ b/pgfexamples/equivalence/loopy/trivial_iid.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/equivalence/loopy/trivial_iid.pgcl pgfexamples/equivalence/loopy/invariants/trivial_iid_invariant.pgcl nat n; nat m; nat tmp; diff --git a/pgfexamples/independence/infinite_multiplication.pgcl b/pgfexamples/independence/infinite_multiplication.pgcl index f33e6f4..677af4a 100644 --- a/pgfexamples/independence/infinite_multiplication.pgcl +++ b/pgfexamples/independence/infinite_multiplication.pgcl @@ -1,3 +1,5 @@ +# skip +# fails (on purpose) nat x; nat y; nat z; diff --git a/pgfexamples/independence/oblivious_transfer.pgcl b/pgfexamples/independence/oblivious_transfer.pgcl index 3396334..2340186 100644 --- a/pgfexamples/independence/oblivious_transfer.pgcl +++ b/pgfexamples/independence/oblivious_transfer.pgcl @@ -1,3 +1,4 @@ + # 3 bit messages, no real bitwise XOR used, inspirited by Barthe et al., A Probabilistic Separation Logic nat r0; diff --git a/pgfexamples/independence/private_information_retriveal.pgcl b/pgfexamples/independence/private_information_retriveal.pgcl index 136f687..9d7c534 100644 --- a/pgfexamples/independence/private_information_retriveal.pgcl +++ b/pgfexamples/independence/private_information_retriveal.pgcl @@ -1,3 +1,4 @@ + # 3 bit, bitwise, inspirited by Barthe et al., A Probabilistic Separation Logic nat q00; diff --git a/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl b/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl index 18a932e..6eaea6a 100644 --- a/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/burgler_alarm.pgcl nat earthquake; nat burglary; nat alarm; diff --git a/pgfexamples/inference/loop_free/conditioning/caesar.pgcl b/pgfexamples/inference/loop_free/conditioning/caesar.pgcl index aaca59b..a787d66 100644 --- a/pgfexamples/inference/loop_free/conditioning/caesar.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/caesar.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/caesar.pgcl nat key; nat randomChar; nat cipher; diff --git a/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl b/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl index d49d87c..29816d6 100644 --- a/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/conditioning_divergence.pgcl nat x; nat y; diff --git a/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl b/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl index a85c580..8abcec5 100644 --- a/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/digitRecognition.pgcl nat y; nat tmp; diff --git a/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl b/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl index 77c8ef2..39da5e1 100644 --- a/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/evidence1.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/evidence1.pgcl nat evidence; nat coin; diff --git a/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl b/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl index 23e83bf..a1c71fc 100644 --- a/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/evidence2.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/evidence2.pgcl nat evidence; nat coin; nat coin1; diff --git a/pgfexamples/inference/loop_free/conditioning/grass.pgcl b/pgfexamples/inference/loop_free/conditioning/grass.pgcl index 3248ffe..b23a8f2 100644 --- a/pgfexamples/inference/loop_free/conditioning/grass.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/grass.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/grass.pgcl nat cloudy; nat rain; nat sprinkler; diff --git a/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl b/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl index e7d5daf..9b90887 100644 --- a/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/infer_geom_mix.pgcl // sample from either 1, 2, or 3 geom distributions and add the results // infer from how many distributions we sampled based on observing one result diff --git a/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl b/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl index 6f56988..e3bd8b9 100644 --- a/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/lin_regression_unbiased.pgcl nat a; nat b; nat x1; diff --git a/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl b/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl index 3ec7902..2c0a2cc 100644 --- a/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/lucky_throw.pgcl nat die; nat lucky_throw; nat hand; diff --git a/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl b/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl index 759bdc0..b7c9dab 100644 --- a/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/monty_hall_nested.pgcl nat prize; nat player; nat door; diff --git a/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl b/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl index e13ecce..c348ead 100644 --- a/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/murder_mystery.pgcl nat aliceDunnit; nat withGun; rparam p; diff --git a/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl b/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl index 9ea3980..83de75c 100644 --- a/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/skip_lin_regression_biased.pgcl @@ -1,3 +1,4 @@ +# skip nat a; nat b; nat x1; diff --git a/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl b/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl index 9b6ce2a..e72700e 100644 --- a/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/telephone_operator.pgcl nat x; // 0: weekday, 1: weekend nat d; // sample the number of phone calls received in one hour. //rparam p; diff --git a/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl b/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl index e041ed8..1725bb7 100644 --- a/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/twocoins.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/twocoins.pgcl nat firstCoin; nat secondCoin; nat bothHeads; diff --git a/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl b/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl index cfeb2dd..41d587f 100644 --- a/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl +++ b/pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/conditioning/undefined_normalization.pgcl nat x; observe(false) \ No newline at end of file diff --git a/pgfexamples/inference/loop_free/dnd_handicap.pgcl b/pgfexamples/inference/loop_free/dnd_handicap.pgcl index c649b49..c0c5937 100644 --- a/pgfexamples/inference/loop_free/dnd_handicap.pgcl +++ b/pgfexamples/inference/loop_free/dnd_handicap.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/dnd_handicap.pgcl // Estimates benefits or punishments when beeing allowed to throw multiple dice // and take the maximum / mininmum of these dice. The punishment is controlled // by the variable `good`. diff --git a/pgfexamples/inference/loop_free/function.pgcl b/pgfexamples/inference/loop_free/function.pgcl index fb90f56..85a65b0 100644 --- a/pgfexamples/inference/loop_free/function.pgcl +++ b/pgfexamples/inference/loop_free/function.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/function.pgcl fun f := { nat a; return 20*a + 2; diff --git a/pgfexamples/inference/loop_free/fuzzy_or.pgcl b/pgfexamples/inference/loop_free/fuzzy_or.pgcl index f4d2c42..9fb3b1e 100644 --- a/pgfexamples/inference/loop_free/fuzzy_or.pgcl +++ b/pgfexamples/inference/loop_free/fuzzy_or.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/fuzzy_or.pgcl nat n0; nat n1; nat n2; diff --git a/pgfexamples/inference/loop_free/max.pgcl b/pgfexamples/inference/loop_free/max.pgcl index c480973..7c15875 100644 --- a/pgfexamples/inference/loop_free/max.pgcl +++ b/pgfexamples/inference/loop_free/max.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/max.pgcl fun max := { nat x; nat y; diff --git a/pgfexamples/inference/loop_free/monty_hall.pgcl b/pgfexamples/inference/loop_free/monty_hall.pgcl index 8cc9254..e2ae780 100644 --- a/pgfexamples/inference/loop_free/monty_hall.pgcl +++ b/pgfexamples/inference/loop_free/monty_hall.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/monty_hall.pgcl nat prize; nat player; nat opendoor; diff --git a/pgfexamples/inference/loop_free/pi.pgcl b/pgfexamples/inference/loop_free/pi.pgcl index c35b2fa..4254e8c 100644 --- a/pgfexamples/inference/loop_free/pi.pgcl +++ b/pgfexamples/inference/loop_free/pi.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/pi.pgcl nat x nat y x := unif(0,30) diff --git a/pgfexamples/inference/loop_free/piranha.pgcl b/pgfexamples/inference/loop_free/piranha.pgcl index 4987f1c..11ef4dd 100644 --- a/pgfexamples/inference/loop_free/piranha.pgcl +++ b/pgfexamples/inference/loop_free/piranha.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/piranha.pgcl nat piranha nat fish_taken_is_piranha diff --git a/pgfexamples/inference/loop_free/poor_scale.pgcl b/pgfexamples/inference/loop_free/poor_scale.pgcl index 4298df0..98e9ff5 100644 --- a/pgfexamples/inference/loop_free/poor_scale.pgcl +++ b/pgfexamples/inference/loop_free/poor_scale.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/poor_scale.pgcl nat n; nat x; diff --git a/pgfexamples/inference/loop_free/prob_collatz.pgcl b/pgfexamples/inference/loop_free/prob_collatz.pgcl index 14dc157..a3c06f0 100644 --- a/pgfexamples/inference/loop_free/prob_collatz.pgcl +++ b/pgfexamples/inference/loop_free/prob_collatz.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/prob_collatz.pgcl nat n; nat x; diff --git a/pgfexamples/inference/loop_free/scalability.pgcl b/pgfexamples/inference/loop_free/scalability.pgcl index 9aaa0f2..273729a 100644 --- a/pgfexamples/inference/loop_free/scalability.pgcl +++ b/pgfexamples/inference/loop_free/scalability.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loop_free/scalability.pgcl nat x; x := geometric(1/2); diff --git a/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl b/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl index a4cf45a..ef3083c 100644 --- a/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl +++ b/pgfexamples/inference/loopy/conditioning/dep_bern.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loopy/conditioning/dep_bern.pgcl nat c; nat m; nat n; diff --git a/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl b/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl index 313d80c..8e0124f 100644 --- a/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl +++ b/pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loopy/conditioning/trivial_iid.pgcl nat n; nat m; nat tmp; diff --git a/pgfexamples/inference/loopy/dueling_cowboys.pgcl b/pgfexamples/inference/loopy/dueling_cowboys.pgcl index d785937..8a46e41 100644 --- a/pgfexamples/inference/loopy/dueling_cowboys.pgcl +++ b/pgfexamples/inference/loopy/dueling_cowboys.pgcl @@ -1,3 +1,4 @@ +# main pgfexamples/inference/loopy/dueling_cowboys.pgcl nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable rparam a; // probability that Player A shoots player B in a turn. diff --git a/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl b/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl index 95a22e5..2e19ad9 100644 --- a/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl +++ b/pgfexamples/inference/loopy/skip_exceeding_sum.pgcl @@ -1,3 +1,4 @@ +# skip nat sum; nat c; nat temp; diff --git a/pgfexamples/inference/loopy/skip_geom_dist.pgcl b/pgfexamples/inference/loopy/skip_geom_dist.pgcl index c80656b..1460d83 100644 --- a/pgfexamples/inference/loopy/skip_geom_dist.pgcl +++ b/pgfexamples/inference/loopy/skip_geom_dist.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; diff --git a/pgfexamples/inference/loopy/skip_random_walk.pgcl b/pgfexamples/inference/loopy/skip_random_walk.pgcl index 5d1fe5f..3079269 100644 --- a/pgfexamples/inference/loopy/skip_random_walk.pgcl +++ b/pgfexamples/inference/loopy/skip_random_walk.pgcl @@ -1,3 +1,4 @@ +# skip // Currently leads to issues! nat x; diff --git a/pgfexamples/inference/loopy/uniform_sampling.pgcl b/pgfexamples/inference/loopy/uniform_sampling.pgcl index 3f2181f..6488aae 100644 --- a/pgfexamples/inference/loopy/uniform_sampling.pgcl +++ b/pgfexamples/inference/loopy/uniform_sampling.pgcl @@ -1,6 +1,7 @@ +# main pgfexamples/inference/loopy/uniform_sampling.pgcl + # correctness proof in [Lumbroso 2013] # invariant most likely not in loop-free ReDiP-Fragment. - nat running; nat v; nat c; diff --git a/pgfexamples/invariant_synthesis/cond_and.pgcl b/pgfexamples/invariant_synthesis/cond_and.pgcl index 06b8c67..65155f6 100644 --- a/pgfexamples/invariant_synthesis/cond_and.pgcl +++ b/pgfexamples/invariant_synthesis/cond_and.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/cond_and.pgcl nat m; nat n; diff --git a/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl index 7954b21..2e84b8f 100644 --- a/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl +++ b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/fast_dice_roller.pgcl nat v; nat c; bool flag; diff --git a/pgfexamples/invariant_synthesis/faulty_decrement.pgcl b/pgfexamples/invariant_synthesis/faulty_decrement.pgcl index f7d42e8..4aeed3c 100644 --- a/pgfexamples/invariant_synthesis/faulty_decrement.pgcl +++ b/pgfexamples/invariant_synthesis/faulty_decrement.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/faulty_decrement.pgcl nat x; x := geometric(1/2) diff --git a/pgfexamples/invariant_synthesis/geometric.pgcl b/pgfexamples/invariant_synthesis/geometric.pgcl index e011901..f66f954 100644 --- a/pgfexamples/invariant_synthesis/geometric.pgcl +++ b/pgfexamples/invariant_synthesis/geometric.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/geometric.pgcl nat x; x := 1 diff --git a/pgfexamples/invariant_synthesis/geometric_counter.pgcl b/pgfexamples/invariant_synthesis/geometric_counter.pgcl index 06e5d88..38b095c 100644 --- a/pgfexamples/invariant_synthesis/geometric_counter.pgcl +++ b/pgfexamples/invariant_synthesis/geometric_counter.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/geometric_counter.pgcl nat x; nat c; diff --git a/pgfexamples/invariant_synthesis/modulo_geometric.pgcl b/pgfexamples/invariant_synthesis/modulo_geometric.pgcl index 7922e91..44ad390 100644 --- a/pgfexamples/invariant_synthesis/modulo_geometric.pgcl +++ b/pgfexamples/invariant_synthesis/modulo_geometric.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/modulo_geometric.pgcl nat x; x := geometric(1/2) diff --git a/pgfexamples/invariant_synthesis/nontermination.pgcl b/pgfexamples/invariant_synthesis/nontermination.pgcl index 49464c2..01b4ce5 100644 --- a/pgfexamples/invariant_synthesis/nontermination.pgcl +++ b/pgfexamples/invariant_synthesis/nontermination.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/nontermination.pgcl nat x; {x:=1}[1/2]{x:=2} diff --git a/pgfexamples/invariant_synthesis/random_walk.pgcl b/pgfexamples/invariant_synthesis/random_walk.pgcl index 88f72f9..9334be1 100644 --- a/pgfexamples/invariant_synthesis/random_walk.pgcl +++ b/pgfexamples/invariant_synthesis/random_walk.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/random_walk.pgcl nat x; x := 1 diff --git a/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl b/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl index 7a3a11e..32d099b 100644 --- a/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl +++ b/pgfexamples/invariant_synthesis/skip_random_walk_counter.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; diff --git a/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl b/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl index d3c1942..a83a446 100644 --- a/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl +++ b/pgfexamples/invariant_synthesis/skip_sequential_loops.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; diff --git a/pgfexamples/invariant_synthesis/subdist_enter.pgcl b/pgfexamples/invariant_synthesis/subdist_enter.pgcl index 726b258..ac4dca8 100644 --- a/pgfexamples/invariant_synthesis/subdist_enter.pgcl +++ b/pgfexamples/invariant_synthesis/subdist_enter.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/subdist_enter.pgcl nat x; {x:=1}[1/2]{x:=3} diff --git a/pgfexamples/invariant_synthesis/thirds_geometric.pgcl b/pgfexamples/invariant_synthesis/thirds_geometric.pgcl index a8c3ac1..6a4834b 100644 --- a/pgfexamples/invariant_synthesis/thirds_geometric.pgcl +++ b/pgfexamples/invariant_synthesis/thirds_geometric.pgcl @@ -1,3 +1,4 @@ +# invariant_synthesis pgfexamples/invariant_synthesis/thirds_geometric.pgcl nat x; x := 1 diff --git a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl index 599a593..bca9394 100644 --- a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/bit_flip_conditioning_generalized_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl bool b1 bool b2 bool b3 diff --git a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl index 784f9f1..a1eff73 100644 --- a/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/bit_flip_conditioning_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl bool b1 bool b2 bool b3 diff --git a/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl b/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl index f859b98..d40d052 100644 --- a/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/brp_obs_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl nat s; nat f; nat h; diff --git a/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl b/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl index 99212fc..5b5b9fa 100644 --- a/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/dueling_cowboys_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable rparam a; // probability that Player A shoots player B in a turn. diff --git a/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl b/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl index cbe77b8..bec7251 100644 --- a/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/geometric_observe_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl nat y; nat x; nat tmp; diff --git a/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl b/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl index 92975a7..325430b 100644 --- a/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/geometric_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl nat x; nat c; nat temp; diff --git a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl index 8c8cb76..c0d0f94 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_generalized_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip bool b1 bool b2 bool b3 diff --git a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl index 8832330..76af342 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/bit_flip_conditioning_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip bool b1 bool b2 bool b3 diff --git a/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl index 46bb669..038f0fb 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/brp_obs_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat s; nat f; nat h; diff --git a/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl index 257a4df..13e0fa1 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/dueling_cowboys_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable rparam a; // probability that Player A shoots player B in a turn. diff --git a/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl index 209b2c7..108801b 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/geometric_observe_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat y; nat x; nat tmp; diff --git a/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl index b8f6a56..2111a46 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/geometric_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat x; nat c; nat temp; diff --git a/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl index 6f3fff8..ca04c9a 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat s; nat die; rparam p; diff --git a/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl index 782d9ac..61e3d2e 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat n; nat c; nat tmp; diff --git a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl index 2feed46..c4fad66 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat n; nat i; nat temp; diff --git a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl index 2feed46..c4fad66 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat n; nat i; nat temp; diff --git a/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl b/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl index 3a5507f..0be24e5 100644 --- a/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl +++ b/pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl @@ -1,3 +1,4 @@ +# skip nat s; nat c; nat tmp; diff --git a/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl b/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl index b9e51c0..211f1a0 100644 --- a/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/ky_die_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/ky_die_parameter_invariant.pgcl nat s; nat die; diff --git a/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl b/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl index e6a9f09..4084f51 100644 --- a/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/n_geometric_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/n_geometric_parameter_invariant.pgcl nat n; nat c; nat tmp; diff --git a/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl b/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl index c8d1bce..e8d6546 100644 --- a/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/negative_binomial_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/negative_binomial_parameter_invariant.pgcl nat n; nat i; nat temp; diff --git a/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl b/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl index e671bbd..a2eea38 100644 --- a/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/negative_binomial_reversed_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/negative_binomial_reversed_parameter_invariant.pgcl nat n; nat i; nat temp; diff --git a/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl b/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl index e85acb9..e97a03d 100644 --- a/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl @@ -1,3 +1,4 @@ +# check_equality pgfexamples/template_parameter_synthesis/random_walk_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/random_walk_parameter_invariant.pgcl nat s; nat c; nat tmp; diff --git a/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl b/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl index 6241038..8960833 100644 --- a/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl +++ b/pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl @@ -1,3 +1,6 @@ +# skip +# TODO this has no invariant file +# check_equality pgfexamples/template_parameter_synthesis/telephone_operator_parameter.pgcl pgfexamples/template_parameter_synthesis/invariants/telephone_operator_parameter_invariant.pgcl nat x; // 0: weekday, 1: weekend nat d; // sample the number of phone calls received in one hour. rparam p; From 68b13ebff4e86262acf7dc9f83fa7a2a52f0b295 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Wed, 15 Jan 2025 10:25:39 +0100 Subject: [PATCH 03/49] changed variable name --- .../analysis/equivalence/equivalence_check.py | 21 +++++++++++-------- 1 file changed, 12 insertions(+), 9 deletions(-) diff --git a/prodigy/analysis/equivalence/equivalence_check.py b/prodigy/analysis/equivalence/equivalence_check.py index 9c1adae..8931c7e 100644 --- a/prodigy/analysis/equivalence/equivalence_check.py +++ b/prodigy/analysis/equivalence/equivalence_check.py @@ -50,7 +50,7 @@ def generate_equivalence_test_distribution( def check_equivalence( program: Program, - invariant: Program, + program2: Program, config: ForwardAnalysisConfig, analyzer: Callable[ [Union[Instr, Sequence[Instr]], ProgramInfo, Distribution, Distribution, ForwardAnalysisConfig], @@ -68,15 +68,18 @@ def check_equivalence( the second order distributions generated by the invariant and the once unrolled while loop of the program. If this difference can be made equal to 0, the programs are equivalent. - .. param config: The configuration. - .. param program: The While-Loop program - .. param invariant: The loop-free invariant - .. returns: Whether the invariant and the program are equivalent. + :param config: The configuration. + :param program: The first program + :param program2: The second program + :params analyzer: The analyzer. + :returns: Whether the invariant and the program are equivalent. """ logger.debug("Checking equivalence.") + + # TODO move this line # First we create the modified input program in order to fit the premise of Park's Lemma - modified_inv = cav_phi(program, invariant) + modified_inv = cav_phi(program, program2) # Now we have to generate an infinite state parametrized distribution for every program variable. test_dist, new_vars = generate_equivalence_test_distribution(program, config) @@ -96,15 +99,15 @@ def check_equivalence( if config.show_intermediate_steps: print(f"\n{Style.YELLOW} Compute the result of the invariant. {Style.RESET}") inv_result, inv_error = analyzer( - invariant.instructions, - ProgramInfo(invariant, so_vars=frozenset(new_vars.keys())), test_dist, + program2.instructions, + ProgramInfo(program2, so_vars=frozenset(new_vars.keys())), test_dist, config.factory.one(*(modified_inv.variables | new_vars.keys())) * 0, config) logger.debug("invariant result:\n%s", inv_result) diff = inv_result - modified_inv_result # Compare them and check whether they are equal. - params = program.parameters.keys() | invariant.parameters.keys() + params = program.parameters.keys() | program2.parameters.keys() solver = SolverType.make(config.solver_type) dist_is_solution, dist_candidates = solver.solve(inv_result.set_parameters(*params), modified_inv_result.set_parameters(*params)) From 6819f248f848080f857d500f693083091f58ee59 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Wed, 15 Jan 2025 10:43:43 +0100 Subject: [PATCH 04/49] add comment --- prodigy/analysis/instructionhandler/while_handler.py | 1 + 1 file changed, 1 insertion(+) diff --git a/prodigy/analysis/instructionhandler/while_handler.py b/prodigy/analysis/instructionhandler/while_handler.py index 5d932dc..6b508f9 100644 --- a/prodigy/analysis/instructionhandler/while_handler.py +++ b/prodigy/analysis/instructionhandler/while_handler.py @@ -290,6 +290,7 @@ def compute( if user_choice == "5": return WhileHandler._evt_invariant(instruction, prog_info, distribution, error_prob, config, analyzer) if user_choice == "6": + # TODO include phi step here? return WhileHandler._evt_invariant_synthesis(instruction, prog_info, distribution, error_prob, config, analyzer) if user_choice == "q": From 74b3c6d49bf70f2ad94ad434f1587a9e3d4a1a79 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 22 Jan 2025 11:11:03 +0100 Subject: [PATCH 05/49] Runtime comparison only if more than 1 engine is selected --- benchmark_comparison.py | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 1a1361c..662ae41 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -8,6 +8,7 @@ import re # All files in the pgfexamples folder +# https://stackoverflow.com/a/18394205 all_files: list[str] = [y for x in os.walk("pgfexamples") for y in glob(os.path.join(x[0], '*.pgcl'))] + [ "example.pgcl"] @@ -95,6 +96,9 @@ def __init__(self, args): elif "pgcl" in input_files: # A single file should be tested self.files = [args.input] + elif os.path.isdir(input_files): + # A folder is given, only test files in the folder + self.files = [y for x in os.walk(args.input) for y in glob(os.path.join(x[0], '*.pgcl'))] else: # A file containing files that should be tested self.files = list(map(str.strip, open(input_files, "r").readlines())) @@ -298,7 +302,8 @@ def benchmark(config: Configuration): # Compare results if at least two engines are selected and file wasn't skipped once (if skip_timeouts is set) if len(config.engine) > 1 and not skipped: - fail = compare_output({engine: times[engine][-1] for engine in config.engine}, instructions, file, config.fail_on_error) + fail = compare_output({engine: times[engine][-1] for engine in config.engine}, instructions, file, + config.fail_on_error) if not fail: print("Results are equal, continuing...") @@ -316,6 +321,12 @@ def benchmark(config: Configuration): def setup_outfile(out_file: str, engine_list: list[str]) -> None: + """ + Creates the output csv file and writes the header. If a file of the same name already exists, rename it to _{i}, + where i is the lowest number such that no file with the name _i exists. + :param out_file: The file to be created. + :param engine_list: The list of engines which are tested. + """ # If file exists, rename it to filename_{i}.extension if os.path.isfile(out_file): i = 1 @@ -345,6 +356,7 @@ def obtain_instructions(file_path: str) -> list[str]: if first_line.startswith("#"): # First line is an instruction parts = list(map(str.strip, first_line.split()[1:])) + # If "skip" is set, the file should be ignored if parts == ["skip"]: return [] return parts @@ -539,7 +551,9 @@ def generate_markdown_table(csv_file: str, engine_list: list[str]) -> None: # Write the average and summary f.write( "|Average|" + "|".join([f"{sum(results[i]) / len(results[i])}" for i in range(len(engine_list))]) + "|\n") - f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n") + # Only add the time comparison if at least 2 engines are selected + if len(engine_list) > 1: + f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n") if __name__ == '__main__': From ec7e57267aa574e686a2f68d51005f5a0627caf9 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 22 Jan 2025 11:15:28 +0100 Subject: [PATCH 06/49] more precise help text --- benchmark_comparison.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 662ae41..be2aa0a 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -127,7 +127,8 @@ def create_parser() -> argparse.ArgumentParser: "input", metavar="INPUT", help="File to be analyzed. If set to \"all\", all files in the pgfexamples folder will be analyzed. " + - "If file does not have a .pgcl extension, it is interpreted to be a file containing files to be tested.", + "If a folder is provided, all files with '.pgcl' extensions in the folder or its subfolders are tested. " + + "If file does not have a .pgcl extension, it is interpreted to be a file containing files to be tested.", type=str ) From ae8b07fe9e630b85f36a1c7493cfaffe63a07f09 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 22 Jan 2025 11:48:38 +0100 Subject: [PATCH 07/49] fixed independent vars call --- prodigy/cli.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prodigy/cli.py b/prodigy/cli.py index 5a5b1f2..7d5dad3 100644 --- a/prodigy/cli.py +++ b/prodigy/cli.py @@ -27,6 +27,7 @@ from prodigy.analysis.exceptions import VerificationError from prodigy.analysis.instructionhandler.program_info import ProgramInfo from prodigy.analysis.solver.solver_type import SolverType +from prodigy.analysis.independence.independence import independent_vars as ivars from prodigy.distribution.distribution import State from prodigy.util.color import Style from prodigy.util.logger import log_setup @@ -193,7 +194,7 @@ def independent_vars(ctx, program_file: IO, compute_exact: bool): raise ValueError(f"Could not compile the Program. {prog}") start = time.perf_counter() - indep_rel: Set[frozenset[Var]] = independent_vars(prog, program_file, compute_exact) + indep_rel: Set[frozenset[Var]] = ivars(prog) #, program_file, compute_exact) stop = time.perf_counter() print(Style.OKBLUE + "Under-approximation: \t" + str(indep_rel) + Style.RESET) From 2e34b211a3659282abd9b73fe295b62736b8acfe Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 22 Jan 2025 12:00:01 +0100 Subject: [PATCH 08/49] added first loop-free equiv example --- pgfexamples/equivalence/loop_free/uniform_sampling.pgcl | 4 ++++ pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl | 4 ++++ 2 files changed, 8 insertions(+) create mode 100644 pgfexamples/equivalence/loop_free/uniform_sampling.pgcl create mode 100644 pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl new file mode 100644 index 0000000..1aaa971 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl @@ -0,0 +1,4 @@ +# check_equality pgfexamples/equivalence/loop_free/uniform_sampling.pgcl pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl +nat x + +x := unif(1,6) \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl new file mode 100644 index 0000000..2cd0c77 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl @@ -0,0 +1,4 @@ +# skip +nat x + +{x:=1}[1/6]{{x:=2}[1/6]{{x:=3}[1/6]{{x:=4}[1/6]{{x:=5}[1/6]{x:=6}}}}} \ No newline at end of file From f2dbd2201f86ed028b8ecc5839dc9835ddfee6ee Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 22 Jan 2025 11:11:03 +0100 Subject: [PATCH 09/49] Runtime comparison only if more than 1 engine is selected --- benchmark_comparison.py | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 1a1361c..662ae41 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -8,6 +8,7 @@ import re # All files in the pgfexamples folder +# https://stackoverflow.com/a/18394205 all_files: list[str] = [y for x in os.walk("pgfexamples") for y in glob(os.path.join(x[0], '*.pgcl'))] + [ "example.pgcl"] @@ -95,6 +96,9 @@ def __init__(self, args): elif "pgcl" in input_files: # A single file should be tested self.files = [args.input] + elif os.path.isdir(input_files): + # A folder is given, only test files in the folder + self.files = [y for x in os.walk(args.input) for y in glob(os.path.join(x[0], '*.pgcl'))] else: # A file containing files that should be tested self.files = list(map(str.strip, open(input_files, "r").readlines())) @@ -298,7 +302,8 @@ def benchmark(config: Configuration): # Compare results if at least two engines are selected and file wasn't skipped once (if skip_timeouts is set) if len(config.engine) > 1 and not skipped: - fail = compare_output({engine: times[engine][-1] for engine in config.engine}, instructions, file, config.fail_on_error) + fail = compare_output({engine: times[engine][-1] for engine in config.engine}, instructions, file, + config.fail_on_error) if not fail: print("Results are equal, continuing...") @@ -316,6 +321,12 @@ def benchmark(config: Configuration): def setup_outfile(out_file: str, engine_list: list[str]) -> None: + """ + Creates the output csv file and writes the header. If a file of the same name already exists, rename it to _{i}, + where i is the lowest number such that no file with the name _i exists. + :param out_file: The file to be created. + :param engine_list: The list of engines which are tested. + """ # If file exists, rename it to filename_{i}.extension if os.path.isfile(out_file): i = 1 @@ -345,6 +356,7 @@ def obtain_instructions(file_path: str) -> list[str]: if first_line.startswith("#"): # First line is an instruction parts = list(map(str.strip, first_line.split()[1:])) + # If "skip" is set, the file should be ignored if parts == ["skip"]: return [] return parts @@ -539,7 +551,9 @@ def generate_markdown_table(csv_file: str, engine_list: list[str]) -> None: # Write the average and summary f.write( "|Average|" + "|".join([f"{sum(results[i]) / len(results[i])}" for i in range(len(engine_list))]) + "|\n") - f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n") + # Only add the time comparison if at least 2 engines are selected + if len(engine_list) > 1: + f.write("Times fastest run|" + "|".join(map(str, no_fastest)) + "|\n") if __name__ == '__main__': From d3a73f035fbe98081f784a223af69f4c61c3bf82 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 22 Jan 2025 11:15:28 +0100 Subject: [PATCH 10/49] more precise help text --- benchmark_comparison.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 662ae41..be2aa0a 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -127,7 +127,8 @@ def create_parser() -> argparse.ArgumentParser: "input", metavar="INPUT", help="File to be analyzed. If set to \"all\", all files in the pgfexamples folder will be analyzed. " + - "If file does not have a .pgcl extension, it is interpreted to be a file containing files to be tested.", + "If a folder is provided, all files with '.pgcl' extensions in the folder or its subfolders are tested. " + + "If file does not have a .pgcl extension, it is interpreted to be a file containing files to be tested.", type=str ) From 0f0d36796426cd7afc57619af141199e0f8d442e Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 22 Jan 2025 11:48:38 +0100 Subject: [PATCH 11/49] fixed independent vars call --- prodigy/cli.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/prodigy/cli.py b/prodigy/cli.py index 5a5b1f2..7d5dad3 100644 --- a/prodigy/cli.py +++ b/prodigy/cli.py @@ -27,6 +27,7 @@ from prodigy.analysis.exceptions import VerificationError from prodigy.analysis.instructionhandler.program_info import ProgramInfo from prodigy.analysis.solver.solver_type import SolverType +from prodigy.analysis.independence.independence import independent_vars as ivars from prodigy.distribution.distribution import State from prodigy.util.color import Style from prodigy.util.logger import log_setup @@ -193,7 +194,7 @@ def independent_vars(ctx, program_file: IO, compute_exact: bool): raise ValueError(f"Could not compile the Program. {prog}") start = time.perf_counter() - indep_rel: Set[frozenset[Var]] = independent_vars(prog, program_file, compute_exact) + indep_rel: Set[frozenset[Var]] = ivars(prog) #, program_file, compute_exact) stop = time.perf_counter() print(Style.OKBLUE + "Under-approximation: \t" + str(indep_rel) + Style.RESET) From f6c0aeacf53a8e96d1142ba6eddd3d633e6db5cf Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 22 Jan 2025 12:00:01 +0100 Subject: [PATCH 12/49] added first loop-free equiv example --- pgfexamples/equivalence/loop_free/uniform_sampling.pgcl | 4 ++++ pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl | 4 ++++ 2 files changed, 8 insertions(+) create mode 100644 pgfexamples/equivalence/loop_free/uniform_sampling.pgcl create mode 100644 pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl new file mode 100644 index 0000000..1aaa971 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl @@ -0,0 +1,4 @@ +# check_equality pgfexamples/equivalence/loop_free/uniform_sampling.pgcl pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl +nat x + +x := unif(1,6) \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl new file mode 100644 index 0000000..2cd0c77 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl @@ -0,0 +1,4 @@ +# skip +nat x + +{x:=1}[1/6]{{x:=2}[1/6]{{x:=3}[1/6]{{x:=4}[1/6]{{x:=5}[1/6]{x:=6}}}}} \ No newline at end of file From df17cdd842f2bb38ae70efd00db3c2108afdac58 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Thu, 23 Jan 2025 16:19:45 +0100 Subject: [PATCH 13/49] moved cov_phi, added check for variable difference --- prodigy/analysis/equivalence/equivalence_check.py | 14 +++++++------- .../analysis/instructionhandler/while_handler.py | 7 ++++++- 2 files changed, 13 insertions(+), 8 deletions(-) diff --git a/prodigy/analysis/equivalence/equivalence_check.py b/prodigy/analysis/equivalence/equivalence_check.py index 8931c7e..7b6240d 100644 --- a/prodigy/analysis/equivalence/equivalence_check.py +++ b/prodigy/analysis/equivalence/equivalence_check.py @@ -77,9 +77,9 @@ def check_equivalence( logger.debug("Checking equivalence.") - # TODO move this line - # First we create the modified input program in order to fit the premise of Park's Lemma - modified_inv = cav_phi(program, program2) + # If both programs do not have the same variables, they are not equal + if set(program.variables.keys()).difference(set(program2.variables.keys())) != set(): + return False, State() # TODO how should the state look like? # Now we have to generate an infinite state parametrized distribution for every program variable. test_dist, new_vars = generate_equivalence_test_distribution(program, config) @@ -87,10 +87,10 @@ def check_equivalence( # Compute the resulting distributions for both programs logger.debug("Compute the modified invariant...") modified_inv_result, modified_inv_error = analyzer( - modified_inv.instructions, - ProgramInfo(modified_inv, so_vars=frozenset(new_vars.keys())), + program2.instructions, + ProgramInfo(program2, so_vars=frozenset(new_vars.keys())), test_dist, - config.factory.from_expr("0", *(modified_inv.variables | new_vars.keys())), + config.factory.from_expr("0", *(program2.variables | new_vars.keys())), config ) logger.debug("modified invariant result:\n%s", modified_inv_result) @@ -101,7 +101,7 @@ def check_equivalence( inv_result, inv_error = analyzer( program2.instructions, ProgramInfo(program2, so_vars=frozenset(new_vars.keys())), test_dist, - config.factory.one(*(modified_inv.variables | new_vars.keys())) * 0, config) + config.factory.one(*(program2.variables | new_vars.keys())) * 0, config) logger.debug("invariant result:\n%s", inv_result) diff = inv_result - modified_inv_result diff --git a/prodigy/analysis/instructionhandler/while_handler.py b/prodigy/analysis/instructionhandler/while_handler.py index 6b508f9..c03b38b 100644 --- a/prodigy/analysis/instructionhandler/while_handler.py +++ b/prodigy/analysis/instructionhandler/while_handler.py @@ -18,6 +18,7 @@ from prodigy.analysis.instructionhandler.program_info import ProgramInfo from prodigy.distribution import Distribution, State from prodigy.distribution.generating_function import SympyPGF +from prodigy.pgcl.pgcl_operations import cav_phi from prodigy.util.color import Style from prodigy.util.logger import print_progress_bar, log_setup @@ -47,8 +48,12 @@ def _analyze_with_invariant( instructions=[instruction], functions=prog_info.functions) print(f"{Style.YELLOW}Verifying invariant...{Style.RESET}") + + # First we create the modified input program in order to fit the premise of Park's Lemma + modified_inv = cav_phi(prog, inv_prog) + answer, result = check_equivalence( - prog, inv_prog, config, analyzer) + prog, modified_inv, config, analyzer) if answer: assert isinstance(result, list) if len(result) == 0: From b7fbec05da17dfbb73d8dff4ea1c0fecaef76caf Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Fri, 24 Jan 2025 17:35:38 +0100 Subject: [PATCH 14/49] refactored equiv check --- .../loop_free/uniform_sampling_2.pgcl | 10 +++- .../analysis/equivalence/equivalence_check.py | 49 ++++++++++--------- prodigy/cli.py | 14 +++--- 3 files changed, 43 insertions(+), 30 deletions(-) diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl index 2cd0c77..f746fc5 100644 --- a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl +++ b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl @@ -1,4 +1,12 @@ # skip nat x -{x:=1}[1/6]{{x:=2}[1/6]{{x:=3}[1/6]{{x:=4}[1/6]{{x:=5}[1/6]{x:=6}}}}} \ No newline at end of file +{x:=1}[1/6]{ + {x:=2}[1/5]{ + {x:=3}[1/4]{ + {x:=4}[1/3]{ + {x:=5}[1/2]{x:=6} + } + } + } +} \ No newline at end of file diff --git a/prodigy/analysis/equivalence/equivalence_check.py b/prodigy/analysis/equivalence/equivalence_check.py index 7b6240d..a9501f2 100644 --- a/prodigy/analysis/equivalence/equivalence_check.py +++ b/prodigy/analysis/equivalence/equivalence_check.py @@ -50,7 +50,7 @@ def generate_equivalence_test_distribution( def check_equivalence( program: Program, - program2: Program, + other_program: Program, config: ForwardAnalysisConfig, analyzer: Callable[ [Union[Instr, Sequence[Instr]], ProgramInfo, Distribution, Distribution, ForwardAnalysisConfig], @@ -70,7 +70,7 @@ def check_equivalence( equivalent. :param config: The configuration. :param program: The first program - :param program2: The second program + :param other_program: The second program :params analyzer: The analyzer. :returns: Whether the invariant and the program are equivalent. """ @@ -78,41 +78,46 @@ def check_equivalence( logger.debug("Checking equivalence.") # If both programs do not have the same variables, they are not equal - if set(program.variables.keys()).difference(set(program2.variables.keys())) != set(): + if set(program.variables.keys()).difference(set(other_program.variables.keys())) != set(): + logger.info("The two programs already have different variable sets, prog: %s, other: %s", + program.variables.keys(), other_program.variables.keys()) return False, State() # TODO how should the state look like? # Now we have to generate an infinite state parametrized distribution for every program variable. test_dist, new_vars = generate_equivalence_test_distribution(program, config) # Compute the resulting distributions for both programs - logger.debug("Compute the modified invariant...") - modified_inv_result, modified_inv_error = analyzer( - program2.instructions, - ProgramInfo(program2, so_vars=frozenset(new_vars.keys())), + logger.debug("Compute the other programs posterior...") + other_program_posterior, other_program_error = analyzer( + other_program.instructions, + ProgramInfo(other_program, so_vars=frozenset(new_vars.keys())), test_dist, - config.factory.from_expr("0", *(program2.variables | new_vars.keys())), + config.factory.from_expr("0", *(other_program.variables | new_vars.keys())), config ) - logger.debug("modified invariant result:\n%s", modified_inv_result) - logger.debug("Compute the invariant...") + logger.debug("other programs result:\n%s", other_program_posterior) + logger.debug("Compute the posterior of the program...") if config.show_intermediate_steps: - print(f"\n{Style.YELLOW} Compute the result of the invariant. {Style.RESET}") - inv_result, inv_error = analyzer( - program2.instructions, - ProgramInfo(program2, so_vars=frozenset(new_vars.keys())), test_dist, - config.factory.one(*(program2.variables | new_vars.keys())) * 0, config) - logger.debug("invariant result:\n%s", inv_result) + print(f"\n{Style.YELLOW} Compute the posterior of the program. {Style.RESET}") + program_posterior, program_error = analyzer( + program.instructions, + ProgramInfo(program, so_vars=frozenset(new_vars.keys())), + test_dist, + config.factory.one(*(program.variables | new_vars.keys())) * 0, + config + ) + logger.debug("program result:\n%s", program_posterior) - diff = inv_result - modified_inv_result + diff = program_posterior - other_program_posterior # Compare them and check whether they are equal. - params = program.parameters.keys() | program2.parameters.keys() + params = program.parameters.keys() | other_program.parameters.keys() solver = SolverType.make(config.solver_type) - dist_is_solution, dist_candidates = solver.solve(inv_result.set_parameters(*params), - modified_inv_result.set_parameters(*params)) - err_is_solution, err_candidates = solver.solve(inv_error.set_parameters(*params), - modified_inv_error.set_parameters(*params)) + dist_is_solution, dist_candidates = solver.solve(program_posterior.set_parameters(*params), + other_program_posterior.set_parameters(*params)) + err_is_solution, err_candidates = solver.solve(program_error.set_parameters(*params), + other_program_error.set_parameters(*params)) # If there is no solution tell the user why. if (dist_is_solution and err_is_solution) is False: diff --git a/prodigy/cli.py b/prodigy/cli.py index 7d5dad3..44e1fd2 100644 --- a/prodigy/cli.py +++ b/prodigy/cli.py @@ -126,8 +126,8 @@ def main(ctx, program_file: IO, input_dist: str, @cli.command('check_equality') @click.pass_context @click.argument('program_file', type=click.File('r')) -@click.argument('invariant_file', type=click.File('r')) -def check_equality(ctx, program_file: IO, invariant_file: IO): +@click.argument('other_program_file', type=click.File('r')) +def check_equality(ctx, program_file: IO, other_program_file: IO): """ Checks whether a certain loop-free program is an invariant of a specified while loop. :param program_file: the file containing the while-loop @@ -135,18 +135,18 @@ def check_equality(ctx, program_file: IO, invariant_file: IO): :return: """ prog_src = program_file.read() - inv_src = invariant_file.read() + other_prog_src = other_program_file.read() prog = compiler.parse_pgcl(prog_src) if isinstance(prog, CheckFail): raise ValueError(f"Could not compile the Program. {prog}") - inv = compiler.parse_pgcl(inv_src) - if isinstance(inv, CheckFail): - raise ValueError(f"Could not compile invariant. {inv}") + other_prog = compiler.parse_pgcl(other_prog_src) + if isinstance(other_prog, CheckFail): + raise ValueError(f"Could not compile invariant. {other_prog}") start = time.perf_counter() - equiv, result = check_equivalence(prog, inv, ctx.obj['CONFIG'], compute_semantics) + equiv, result = check_equivalence(prog, other_prog, ctx.obj['CONFIG'], compute_semantics) stop = time.perf_counter() if equiv is True: assert isinstance(result, list) From 19640c1efb32e67f991946bb00f7c4dece2c8c6d Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Fri, 24 Jan 2025 17:36:28 +0100 Subject: [PATCH 15/49] deleted --- pgfexamples/equivalence/loop_free/.gitkeep | 0 1 file changed, 0 insertions(+), 0 deletions(-) delete mode 100644 pgfexamples/equivalence/loop_free/.gitkeep diff --git a/pgfexamples/equivalence/loop_free/.gitkeep b/pgfexamples/equivalence/loop_free/.gitkeep deleted file mode 100644 index e69de29..0000000 From 4878983eedd2e9d1816a8ba6c28231f1d34ccb2a Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Fri, 24 Jan 2025 17:50:27 +0100 Subject: [PATCH 16/49] fixed --- prodigy/analysis/instructionhandler/while_handler.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prodigy/analysis/instructionhandler/while_handler.py b/prodigy/analysis/instructionhandler/while_handler.py index c03b38b..b515524 100644 --- a/prodigy/analysis/instructionhandler/while_handler.py +++ b/prodigy/analysis/instructionhandler/while_handler.py @@ -53,7 +53,7 @@ def _analyze_with_invariant( modified_inv = cav_phi(prog, inv_prog) answer, result = check_equivalence( - prog, modified_inv, config, analyzer) + inv_prog, modified_inv, config, analyzer) if answer: assert isinstance(result, list) if len(result) == 0: From 28f0bfb1ff0871611ad831bda462f977de25af52 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Fri, 24 Jan 2025 17:51:30 +0100 Subject: [PATCH 17/49] minor --- prodigy/analysis/instructionhandler/while_handler.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prodigy/analysis/instructionhandler/while_handler.py b/prodigy/analysis/instructionhandler/while_handler.py index b515524..4998f21 100644 --- a/prodigy/analysis/instructionhandler/while_handler.py +++ b/prodigy/analysis/instructionhandler/while_handler.py @@ -50,10 +50,10 @@ def _analyze_with_invariant( print(f"{Style.YELLOW}Verifying invariant...{Style.RESET}") # First we create the modified input program in order to fit the premise of Park's Lemma - modified_inv = cav_phi(prog, inv_prog) + phi_inv = cav_phi(prog, inv_prog) answer, result = check_equivalence( - inv_prog, modified_inv, config, analyzer) + inv_prog, phi_inv, config, analyzer) if answer: assert isinstance(result, list) if len(result) == 0: From fb40b98c32326bae5371c8f4d00fce56060e289b Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Fri, 24 Jan 2025 17:55:07 +0100 Subject: [PATCH 18/49] minor --- prodigy/analysis/equivalence/equivalence_check.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/prodigy/analysis/equivalence/equivalence_check.py b/prodigy/analysis/equivalence/equivalence_check.py index a9501f2..d3ced29 100644 --- a/prodigy/analysis/equivalence/equivalence_check.py +++ b/prodigy/analysis/equivalence/equivalence_check.py @@ -121,17 +121,17 @@ def check_equivalence( # If there is no solution tell the user why. if (dist_is_solution and err_is_solution) is False: - logger.debug("Invariant validation failed.") + logger.debug("Equivalence refuted.") state, _ = diff.get_state() return False, State({var: state[sym] for sym, var in new_vars.items()}) # If there is a solution, individually, see whether they match. if (dist_is_solution and err_is_solution) is True: if not dist_candidates: - logger.debug("Invariant validated.") + logger.debug("Posterior equivalence validated.") return True, err_candidates if not err_candidates: - logger.debug("Invariant validated.") + logger.debug("Posterior error validated.") return True, dist_candidates logger.debug("Matching individual solutions\n%s\n%s", dist_candidates, err_candidates) res_both = [] @@ -146,5 +146,7 @@ def check_equivalence( logger.debug("Current partial solution space: %s", res_both) if len(res_both) == 0: return False, State() # TODO how to generate a counterexample here? + logger.debug("Equivalence validated.") return True, res_both + logger.debug("Equivalence unknown.") return None, diff From 1e077dfe1481a4bab8ab1f003176dffc254360e6 Mon Sep 17 00:00:00 2001 From: Dominik Date: Tue, 4 Feb 2025 10:03:27 +0100 Subject: [PATCH 19/49] small example --- pgfexamples/README.md | 3 +-- pgfexamples/equivalence/loop_free/bernoulli.pgcl | 4 ++++ pgfexamples/equivalence/loop_free/bernoulli2.pgcl | 4 ++++ pgfexamples/equivalence/loop_free/invariants/.gitkeep | 0 test.pgcl | 10 ++++++++++ 5 files changed, 19 insertions(+), 2 deletions(-) create mode 100644 pgfexamples/equivalence/loop_free/bernoulli.pgcl create mode 100644 pgfexamples/equivalence/loop_free/bernoulli2.pgcl delete mode 100644 pgfexamples/equivalence/loop_free/invariants/.gitkeep create mode 100644 test.pgcl diff --git a/pgfexamples/README.md b/pgfexamples/README.md index 86dfb50..80333c6 100644 --- a/pgfexamples/README.md +++ b/pgfexamples/README.md @@ -10,8 +10,7 @@ pgfexamples/ │   ├── inference │   └── psi_fails # Examples where Psi fails ├── equivalence # Equivalence of two programs -│   ├── loop_free # Programs without loops -│   └── invariants # ... and their counterparts +│   ├── loop_free # Programs without loops and their counterparts │   └── loopy # Programs with loops │   └── invariants # ... and their loop-free counterpart ├── independence # Checks for independent variables diff --git a/pgfexamples/equivalence/loop_free/bernoulli.pgcl b/pgfexamples/equivalence/loop_free/bernoulli.pgcl new file mode 100644 index 0000000..0a3d2e3 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/bernoulli.pgcl @@ -0,0 +1,4 @@ +# check_equality pgfexamples/equivalence/loop_free/bernoulli.pgcl pgfexamples/equivalence/loop_free/bernoulli2.pgcl +nat x; + +{ x := 0 } [1/3] { x := 1 } \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/bernoulli2.pgcl b/pgfexamples/equivalence/loop_free/bernoulli2.pgcl new file mode 100644 index 0000000..17d24fd --- /dev/null +++ b/pgfexamples/equivalence/loop_free/bernoulli2.pgcl @@ -0,0 +1,4 @@ +# skip +nat x; + +x := bernoulli(2/3); \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/invariants/.gitkeep b/pgfexamples/equivalence/loop_free/invariants/.gitkeep deleted file mode 100644 index e69de29..0000000 diff --git a/test.pgcl b/test.pgcl new file mode 100644 index 0000000..7ecbdd1 --- /dev/null +++ b/test.pgcl @@ -0,0 +1,10 @@ +nat x; + + +x := bernoulli(1/3); + +if(x = 0) { + x := 1; +} else { + x := 0; +} From e69fc2ac9c7024564e200c3d8c44e45fcf8ad0a6 Mon Sep 17 00:00:00 2001 From: Dominik Date: Tue, 4 Feb 2025 10:03:44 +0100 Subject: [PATCH 20/49] small example --- test.pgcl | 10 ---------- 1 file changed, 10 deletions(-) delete mode 100644 test.pgcl diff --git a/test.pgcl b/test.pgcl deleted file mode 100644 index 7ecbdd1..0000000 --- a/test.pgcl +++ /dev/null @@ -1,10 +0,0 @@ -nat x; - - -x := bernoulli(1/3); - -if(x = 0) { - x := 1; -} else { - x := 0; -} From 7b1eb64dbcf4c2fdc262a0d4718328e3e2b64646 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 5 Feb 2025 10:14:50 +0100 Subject: [PATCH 21/49] added mockup test for new equality check --- .../equivalence/test_equivalence_check.py | 31 +++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index a842d19..73863bd 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -1,3 +1,5 @@ +import builtins + import pytest import sympy from probably.pgcl.ast import Program @@ -37,6 +39,7 @@ def test_equivalence_check(engine): } else {skip} """) assert isinstance(inv, Program) + res, subs = check_equivalence(prog, inv, ForwardAnalysisConfig(engine=engine), compute_semantics) assert res assert subs == [] @@ -77,3 +80,31 @@ def test_equivalence_check_parameter(engine): assert res assert len(subs) == 1 assert sympy.S(subs[0][sympy.S('p')]) == sympy.S('0.5') or sympy.S(subs[0][sympy.S('p')]) == sympy.S('1/2') + +@pytest.mark.parametrize( + 'engine', + [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, + ForwardAnalysisConfig.Engine.SYMENGINE]) +def test_equivalence_file(monkeypatch, engine): + # Read the body of the program files + with open("pgfexamples/equivalence/loop_free/bernoulli.pgcl", "r") as f: + file = "\n".join(f.readlines()) + + with open("pgfexamples/equivalence/loop_free/bernoulli2.pgcl", "r") as f: + inv = "\n".join(f.readlines()) + + # Compile them to a program object + prog1 = compile_pgcl(file) + prog2 = compile_pgcl(inv) + + assert(isinstance(prog1, Program)) + assert(isinstance(prog2, Program)) + + # Simulate the input for the invariant files + monkeypatch.setattr(builtins, "input", lambda _: "pgfexamples/equivalence/loop_free/bernoulli2.pgcl") + + # Run the main program + res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) + assert res + assert subs == [] + From b0bb58dd1320932fe1ad046f243d6f18719088db Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 5 Feb 2025 10:29:43 +0100 Subject: [PATCH 22/49] fixed broken equivalence tests --- pgfexamples/invariant_synthesis/fast_dice_roller.pgcl | 2 +- tests/analysis/equivalence/test_equivalence_check.py | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl index 2e84b8f..9faaed2 100644 --- a/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl +++ b/pgfexamples/invariant_synthesis/fast_dice_roller.pgcl @@ -22,7 +22,7 @@ while (flag = 0) { flag := 0 v := 0 -!Plot[c, \infty] +#!Plot[c, \infty] // Invariant template seems to be: a*v^4*flag*(1+c+c^2)+b*v^2*(1+c)+d*v with solution: [{a: 1/3, b: 2/3, d: 4/3}] diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 73863bd..2d165e6 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -8,6 +8,7 @@ from prodigy.analysis.analyzer import compute_semantics from prodigy.analysis.config import ForwardAnalysisConfig from prodigy.analysis.equivalence.equivalence_check import check_equivalence +from prodigy.pgcl.pgcl_operations import cav_phi @pytest.mark.parametrize( @@ -40,7 +41,8 @@ def test_equivalence_check(engine): """) assert isinstance(inv, Program) - res, subs = check_equivalence(prog, inv, ForwardAnalysisConfig(engine=engine), compute_semantics) + phi_inv = cav_phi(prog, inv) + res, subs = check_equivalence(phi_inv, inv, ForwardAnalysisConfig(engine=engine), compute_semantics) assert res assert subs == [] @@ -76,7 +78,9 @@ def test_equivalence_check_parameter(engine): } else {skip} """) assert isinstance(inv, Program) - res, subs = check_equivalence(prog, inv, ForwardAnalysisConfig(engine=engine), compute_semantics) + + phi_inv = cav_phi(prog, inv) + res, subs = check_equivalence(phi_inv, inv, ForwardAnalysisConfig(engine=engine), compute_semantics) assert res assert len(subs) == 1 assert sympy.S(subs[0][sympy.S('p')]) == sympy.S('0.5') or sympy.S(subs[0][sympy.S('p')]) == sympy.S('1/2') From 59b4de0f8bfaafb156aa4137ff196b2c80385746 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 5 Feb 2025 10:31:36 +0100 Subject: [PATCH 23/49] name change --- tests/analysis/equivalence/test_equivalence_check.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 2d165e6..f95560a 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -14,7 +14,7 @@ @pytest.mark.parametrize( 'engine', [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, ForwardAnalysisConfig.Engine.SYMENGINE]) -def test_equivalence_check(engine): +def test_equivalence_check_geometric_sampler(engine): prog = compile_pgcl(""" nat x; nat c; From 63c23ca937f32b1082b1c48d0fa314b5506c00f3 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Thu, 6 Feb 2025 11:50:57 +0100 Subject: [PATCH 24/49] optional type --- prodigy/pgcl/pgcl_operations.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prodigy/pgcl/pgcl_operations.py b/prodigy/pgcl/pgcl_operations.py index 94503e3..bc83cf1 100644 --- a/prodigy/pgcl/pgcl_operations.py +++ b/prodigy/pgcl/pgcl_operations.py @@ -16,8 +16,8 @@ def make_else_if(instructions: List[Tuple[BinopExpr, List[Instr]]]) -> IfInstr: """Creates an else-if chain from a list of conditions and bodies for if-instructions""" - outer_instr: IfInstr = None - curr_instr: IfInstr = None + outer_instr: IfInstr | None = None + curr_instr: IfInstr | None = None for cond, body in instructions: instr = IfInstr(cond=cond, true=body, false=None) if outer_instr is None: From 41df41e6276bcfead142f1523e3f68c097170d93 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Fri, 7 Feb 2025 13:06:08 +0100 Subject: [PATCH 25/49] added automatic benchmark tests & doc regarding file structure + naming convention --- pgfexamples/README.md | 27 +++++++- ...sampling_2.pgcl => uniform_sampling2.pgcl} | 0 pgfexamples/equivalence/loopy/condand.pgcl | 2 +- .../equivalence/test_equivalence_check.py | 66 ++++++++++++++++--- 4 files changed, 83 insertions(+), 12 deletions(-) rename pgfexamples/equivalence/loop_free/{uniform_sampling_2.pgcl => uniform_sampling2.pgcl} (100%) diff --git a/pgfexamples/README.md b/pgfexamples/README.md index 80333c6..7d44df4 100644 --- a/pgfexamples/README.md +++ b/pgfexamples/README.md @@ -22,4 +22,29 @@ pgfexamples/ ├── invariant_synthesis # Synthesis of (expected visiting time) invariants └── template_parameter_synthesis # Equality of loopy and loop-free programs with parameters └── invariants # Corresponding loop-free programs -``` \ No newline at end of file +``` + +## File structure + +* Files have a comment in the first line indicating which arguments should be used in order to execute it + +> ```bash +>python prodigy/cli.py METHOD FILE ARGS +>``` +> results in +>``` +># METHOD FILE ARGS +>``` +> in the first line of the corresponding program or just +> ``` +> # skip +> ``` +> if the file should not be automatically tested. + +* Naming convention: + * In `pgfexamples/equivalence/loop_free` the files are named `file_name.pgcl` for the first and + `file_name2.pgcl` for the second program + * In `pgfexamples/equivalence/loopy` and `pgfexamples/template_parameter_synthesis` the files are named + `file_name.pgcl` in the main folder and their corresponding invariants with `file_name_invariant.pgcl` in the + invariants folder + * Invariants and second programs are to be marked with `skip` \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl similarity index 100% rename from pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl rename to pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl diff --git a/pgfexamples/equivalence/loopy/condand.pgcl b/pgfexamples/equivalence/loopy/condand.pgcl index 357a340..cd83060 100644 --- a/pgfexamples/equivalence/loopy/condand.pgcl +++ b/pgfexamples/equivalence/loopy/condand.pgcl @@ -1,4 +1,4 @@ -# check_equality pgfexamples/equivalence/loopy/condard.pgcl pgfexamples/equivalence/loopy/invariants/condard_invariant.pgcl +# skip nat n; nat m; diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index f95560a..8ca8c23 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -1,5 +1,6 @@ import builtins - +import os +from glob import glob import pytest import sympy from probably.pgcl.ast import Program @@ -85,30 +86,75 @@ def test_equivalence_check_parameter(engine): assert len(subs) == 1 assert sympy.S(subs[0][sympy.S('p')]) == sympy.S('0.5') or sympy.S(subs[0][sympy.S('p')]) == sympy.S('1/2') + @pytest.mark.parametrize( - 'engine', + "engine", [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, - ForwardAnalysisConfig.Engine.SYMENGINE]) -def test_equivalence_file(monkeypatch, engine): + ForwardAnalysisConfig.Engine.SYMENGINE] +) +@pytest.mark.parametrize( + "file_path", + [y for x in os.walk("pgfexamples/equivalence/loop_free") for y in glob(os.path.join(x[0], '*.pgcl')) if + not y.endswith('2.pgcl')] +) +def test_equivalence_loop_free_benchmarks(monkeypatch, engine, file_path): # Read the body of the program files - with open("pgfexamples/equivalence/loop_free/bernoulli.pgcl", "r") as f: + with open(file_path, "r") as f: file = "\n".join(f.readlines()) + file2_path = file_path.replace(".pgcl", "2.pgcl") + with open(file2_path, "r") as f: + inv = "\n".join(f.readlines()) + + # Compile them to a program object + prog1 = compile_pgcl(file) + prog2 = compile_pgcl(inv) + + assert (isinstance(prog1, Program)) + assert (isinstance(prog2, Program)) + + # Run the main program + res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) + assert res + assert subs == [] + + +@pytest.mark.parametrize( + "engine", + [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, + #ForwardAnalysisConfig.Engine.SYMENGINE + ] +) +@pytest.mark.parametrize( + "file_path", + [y for x in os.walk("pgfexamples/equivalence/loopy") for y in glob(os.path.join(x[0], '*.pgcl')) if + not "invariants" in y] +) +def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): + # Read the body of the program files + with open(file_path, "r") as f: + lines = f.readlines() + if "skip" in lines[0]: + pytest.skip("File marked as skipped") + file = "\n".join(lines) - with open("pgfexamples/equivalence/loop_free/bernoulli2.pgcl", "r") as f: + invariant_path = file_path.replace("loopy/", "loopy/invariants/").replace(".pgcl", "_invariant.pgcl") + + with open(invariant_path, "r") as f: inv = "\n".join(f.readlines()) # Compile them to a program object prog1 = compile_pgcl(file) prog2 = compile_pgcl(inv) - assert(isinstance(prog1, Program)) - assert(isinstance(prog2, Program)) + assert (isinstance(prog1, Program)) + assert (isinstance(prog2, Program)) + + inputs = iter(["1", invariant_path]) # Simulate the input for the invariant files - monkeypatch.setattr(builtins, "input", lambda _: "pgfexamples/equivalence/loop_free/bernoulli2.pgcl") + monkeypatch.setattr(builtins, "input", lambda _: next(inputs)) # Select invariant file1 # Run the main program res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) assert res assert subs == [] - From 81a390a56377b016e3330bd2a778541ffcef2c7b Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Fri, 7 Feb 2025 13:16:21 +0100 Subject: [PATCH 26/49] benchmark script should now be able to handle interactive programs --- benchmark_comparison.py | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index be2aa0a..4b3b87a 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -239,6 +239,8 @@ def benchmark(config: Configuration): engine_counter = 0 instructions = obtain_instructions(file) + inputs = obtain_inputs(instructions) + skipped = False # For each engine, run the program for engine in config.engine: @@ -262,11 +264,12 @@ def benchmark(config: Configuration): print("File marked to be skipped...") skipped = True continue - # Execute the program + # Execute the program cmd = ["python", "prodigy/cli.py", "--engine", engine, *instructions] + try: - output = subprocess.check_output(cmd, timeout=config.timeout).decode() + output = subprocess.check_output(cmd, timeout=config.timeout, input=inputs).decode() except TimeoutExpired as e: # Command timed out with open("timeouts.txt", "a") as f: @@ -366,6 +369,17 @@ def obtain_instructions(file_path: str) -> list[str]: print(f"No instruction found for {file_path}, executing default instruction...") return default_instruction + [file_path] +def obtain_inputs(instructions: list[str]) -> bytes: + if len(instructions) == 2: + # No input is necessary + return b"" + method = instructions[0] + other_file = instructions[2] + input_cmd = b"" + if method == "check_equality" and ("loopy" in other_file or "template_parameter_synthesis"): + # Select invariant file for loopy programs + input_cmd = b"1\n" + str.encode(other_file + "\n") + return input_cmd def capture_output(output: list[str], cmd: list[str], file: str) -> Run: # Remove ANSI From 4f5c926aee74d78ff620467e2fe1d2ec22e8d6ca Mon Sep 17 00:00:00 2001 From: Dominik Date: Fri, 7 Feb 2025 15:36:46 +0100 Subject: [PATCH 27/49] remove duplicate --- pgfexamples/equivalence/loop_free/uniform_sampling.pgcl | 2 +- pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) delete mode 100644 pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl index 1aaa971..34b31c3 100644 --- a/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl +++ b/pgfexamples/equivalence/loop_free/uniform_sampling.pgcl @@ -1,4 +1,4 @@ -# check_equality pgfexamples/equivalence/loop_free/uniform_sampling.pgcl pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl +# check_equality pgfexamples/equivalence/loop_free/uniform_sampling.pgcl pgfexamples/equivalence/loop_free/uniform_sampling2.pgcl nat x x := unif(1,6) \ No newline at end of file diff --git a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl b/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl deleted file mode 100644 index 2cd0c77..0000000 --- a/pgfexamples/equivalence/loop_free/uniform_sampling_2.pgcl +++ /dev/null @@ -1,4 +0,0 @@ -# skip -nat x - -{x:=1}[1/6]{{x:=2}[1/6]{{x:=3}[1/6]{{x:=4}[1/6]{{x:=5}[1/6]{x:=6}}}}} \ No newline at end of file From de7383a2917df9720375da4e88d8438ad74af8f9 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Wed, 15 Jan 2025 10:55:10 +0100 Subject: [PATCH 28/49] removed duplicates from solutions --- prodigy/analysis/evtinvariants/invariant_synthesis.py | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/prodigy/analysis/evtinvariants/invariant_synthesis.py b/prodigy/analysis/evtinvariants/invariant_synthesis.py index 50279ad..a439508 100644 --- a/prodigy/analysis/evtinvariants/invariant_synthesis.py +++ b/prodigy/analysis/evtinvariants/invariant_synthesis.py @@ -33,7 +33,6 @@ def evt_invariant_synthesis(loop: WhileInstr, # enumerate potential candidates given by a heuristic for evt_candidate in strategy.template_heuristics.generate(): print(f"{Style.YELLOW}Invariant candidate: {evt_candidate}{Style.RESET}{Style.CLEARTOEND}", end="\r") - # Compute one iteration step. evt_inv = evt_candidate one_step_dist, one_step_err = analyzer(loop.body, prog_info, evt_inv.filter(loop.cond), zero_dist, config) @@ -45,13 +44,11 @@ def evt_invariant_synthesis(loop: WhileInstr, solver = SolverType.make(config.solver_type, config.factory) else: solver = SolverType.make(config.solver_type) - # Check equality between the iterated expression and the invariant. logger.debug("Check Invariant candidate %s", evt_inv) is_solution, solution_candidates = solver.solve(evt_inv, phi_inv) if is_solution is False or is_solution is None: continue - logger.debug("Filter solutions in: %s", solution_candidates) # Exclude "all zero" solutions, as well as solutions which make the denominator 0. @@ -65,7 +62,9 @@ def evt_invariant_synthesis(loop: WhileInstr, # which make the denominator zero if denominator.subs(candidate).equals(0): continue - solutions.append(candidate) + + if candidate not in solutions: + solutions.append(candidate) # In case there are still some solutions we check them for actual solutions in the FPS domain with non-negative # coefficients. This is in general a hard problem (not known to be decidable), thus we use heuristics. From 48e274eb71d9d1b0a1096fa9acf811f91df1902a Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Wed, 15 Jan 2025 11:17:46 +0100 Subject: [PATCH 29/49] todos in examples --- pgfexamples/inference/loopy/dueling_cowboys.pgcl | 1 + pgfexamples/inference/loopy/uniform_sampling.pgcl | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/pgfexamples/inference/loopy/dueling_cowboys.pgcl b/pgfexamples/inference/loopy/dueling_cowboys.pgcl index 8a46e41..a9e1d1b 100644 --- a/pgfexamples/inference/loopy/dueling_cowboys.pgcl +++ b/pgfexamples/inference/loopy/dueling_cowboys.pgcl @@ -1,4 +1,5 @@ # main pgfexamples/inference/loopy/dueling_cowboys.pgcl +# TODO How to choose option nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable rparam a; // probability that Player A shoots player B in a turn. diff --git a/pgfexamples/inference/loopy/uniform_sampling.pgcl b/pgfexamples/inference/loopy/uniform_sampling.pgcl index 6488aae..2b1f846 100644 --- a/pgfexamples/inference/loopy/uniform_sampling.pgcl +++ b/pgfexamples/inference/loopy/uniform_sampling.pgcl @@ -1,5 +1,5 @@ # main pgfexamples/inference/loopy/uniform_sampling.pgcl - +# TODO How to choose option # correctness proof in [Lumbroso 2013] # invariant most likely not in loop-free ReDiP-Fragment. nat running; From 015f8e82ab91bceaf97808bcd854110b51250902 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 22 Jan 2025 12:17:03 +0100 Subject: [PATCH 30/49] fixed execution instruction --- pgfexamples/inference/loopy/dueling_cowboys.pgcl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pgfexamples/inference/loopy/dueling_cowboys.pgcl b/pgfexamples/inference/loopy/dueling_cowboys.pgcl index a9e1d1b..798cf34 100644 --- a/pgfexamples/inference/loopy/dueling_cowboys.pgcl +++ b/pgfexamples/inference/loopy/dueling_cowboys.pgcl @@ -1,4 +1,4 @@ -# main pgfexamples/inference/loopy/dueling_cowboys.pgcl +# invariant_syntghesis pgfexamples/inference/loopy/dueling_cowboys.pgcl # TODO How to choose option nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable From 592b6cfd05dc05d90a39dff01e998ad88f42cfb7 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 12 Feb 2025 09:57:34 +0100 Subject: [PATCH 31/49] fixed typo --- pgfexamples/inference/loopy/dueling_cowboys.pgcl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pgfexamples/inference/loopy/dueling_cowboys.pgcl b/pgfexamples/inference/loopy/dueling_cowboys.pgcl index 798cf34..aab44af 100644 --- a/pgfexamples/inference/loopy/dueling_cowboys.pgcl +++ b/pgfexamples/inference/loopy/dueling_cowboys.pgcl @@ -1,4 +1,4 @@ -# invariant_syntghesis pgfexamples/inference/loopy/dueling_cowboys.pgcl +# invariant_synthesis pgfexamples/inference/loopy/dueling_cowboys.pgcl # TODO How to choose option nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable From e9ec07c01a019aaf0b6e85dc63f967ad235f5311 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 12 Feb 2025 10:53:16 +0100 Subject: [PATCH 32/49] fix skip_files --- benchmark_comparison.py | 21 ++++++++++--------- .../dueling_cowboys.pgcl | 3 +-- 2 files changed, 12 insertions(+), 12 deletions(-) rename pgfexamples/{inference/loopy => invariant_synthesis}/dueling_cowboys.pgcl (80%) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 4b3b87a..5f831ed 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -14,11 +14,11 @@ # Timeouts / Exception runs # If files are not present, an empty list is returned -skip_files: list[str] = list(map(str.strip, open("timeouts.txt", "r").readlines())) \ - if os.path.isfile("timeouts.txt") else [] + \ - list(map(str.strip, +skip_files: list[str] = (list(map(str.strip, open("timeouts.txt", "r").readlines())) \ + if os.path.isfile("timeouts.txt") else []) + \ + (list(map(str.strip, open("exceptions.txt", "r").readlines())) if os.path.isfile( - "exceptions.txt") else [] + "exceptions.txt") else []) # All available engines # (will be executed in this order) @@ -239,6 +239,11 @@ def benchmark(config: Configuration): engine_counter = 0 instructions = obtain_instructions(file) + # Check if file is to be skipped + if not instructions: + print("File marked to be skipped...") + continue + inputs = obtain_inputs(instructions) skipped = False @@ -259,12 +264,6 @@ def benchmark(config: Configuration): output = "" - # Check if file is to be skipped - if not instructions: - print("File marked to be skipped...") - skipped = True - continue - # Execute the program cmd = ["python", "prodigy/cli.py", "--engine", engine, *instructions] @@ -272,6 +271,7 @@ def benchmark(config: Configuration): output = subprocess.check_output(cmd, timeout=config.timeout, input=inputs).decode() except TimeoutExpired as e: # Command timed out + print("Command timed out, writing in timeouts.txt...") with open("timeouts.txt", "a") as f: # Write the file in "timeouts.txt" and add to the list f.write(file + "\n") @@ -281,6 +281,7 @@ def benchmark(config: Configuration): raise e continue except subprocess.CalledProcessError as e: + print("Command threw an exception, writing in exceptions.txt...") # Error occurred while running the program (e.g. runtime error) with open("exceptions.txt", "a") as f: # Write the file in "timeouts.txt" and add to the list diff --git a/pgfexamples/inference/loopy/dueling_cowboys.pgcl b/pgfexamples/invariant_synthesis/dueling_cowboys.pgcl similarity index 80% rename from pgfexamples/inference/loopy/dueling_cowboys.pgcl rename to pgfexamples/invariant_synthesis/dueling_cowboys.pgcl index aab44af..66c89db 100644 --- a/pgfexamples/inference/loopy/dueling_cowboys.pgcl +++ b/pgfexamples/invariant_synthesis/dueling_cowboys.pgcl @@ -1,5 +1,4 @@ -# invariant_synthesis pgfexamples/inference/loopy/dueling_cowboys.pgcl -# TODO How to choose option +# invariant_synthesis pgfexamples/invariant_synthesis/dueling_cowboys.pgcl nat t; // t = 0 player A's turn; t = 1 player B's turn; t>1 not interpretable nat c; // c=1, both player alive; c = 0 one player dead; c>1 not interpretable rparam a; // probability that Player A shoots player B in a turn. From 5362f254f401825fc89c27edeea01c259518ad9b Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 12 Feb 2025 11:26:06 +0100 Subject: [PATCH 33/49] fixed parsing error in benchmark script --- benchmark_comparison.py | 2 +- pgfexamples/invariant_synthesis/nontermination.pgcl | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 5f831ed..67232a2 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -415,7 +415,7 @@ def capture_output(output: list[str], cmd: list[str], file: str) -> Run: output = output[1:] return Run( time=float(output[-1].split()[-2]), - output=output[0].split()[1], + output=output[0].split("Invariant: ")[1], file=file ) else: diff --git a/pgfexamples/invariant_synthesis/nontermination.pgcl b/pgfexamples/invariant_synthesis/nontermination.pgcl index 01b4ce5..645c90f 100644 --- a/pgfexamples/invariant_synthesis/nontermination.pgcl +++ b/pgfexamples/invariant_synthesis/nontermination.pgcl @@ -1,4 +1,5 @@ -# invariant_synthesis pgfexamples/invariant_synthesis/nontermination.pgcl +# skip +# --solver z3 invariant_synthesis pgfexamples/invariant_synthesis/nontermination.pgcl nat x; {x:=1}[1/2]{x:=2} From f1e3ea9a31a73f863ba5c183b5a122a45bbea144 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sun, 9 Feb 2025 15:08:11 +0100 Subject: [PATCH 34/49] added new benchmark --- pgfexamples/equivalence/loop_free/dice_sampling.pgcl | 9 +++++++++ pgfexamples/equivalence/loop_free/dice_sampling2.pgcl | 11 +++++++++++ 2 files changed, 20 insertions(+) create mode 100644 pgfexamples/equivalence/loop_free/dice_sampling.pgcl create mode 100644 pgfexamples/equivalence/loop_free/dice_sampling2.pgcl diff --git a/pgfexamples/equivalence/loop_free/dice_sampling.pgcl b/pgfexamples/equivalence/loop_free/dice_sampling.pgcl new file mode 100644 index 0000000..8725265 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/dice_sampling.pgcl @@ -0,0 +1,9 @@ +# check_equality pgfexamples/equivalence/loop_free/dice_sampling.pgcl pgfexamples/equivalence/loop_free/dice_sampling2.pgcl +nat dice; +nat tmp; + +tmp := 0; + +# Roll a dice +dice := unif(1,6); + diff --git a/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl b/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl new file mode 100644 index 0000000..bf248c5 --- /dev/null +++ b/pgfexamples/equivalence/loop_free/dice_sampling2.pgcl @@ -0,0 +1,11 @@ +# skip +nat dice; +nat tmp; + +# Roll a three-sided dice +tmp := unif(1,3); + +# Flip a coin, leave or increase by 3 +{ dice := tmp; } [1/2] { dice := tmp + 3; } + +tmp := 0; \ No newline at end of file From b2429b3061a88e3a27b766682a1dd41fdb28f118 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 12 Feb 2025 11:26:49 +0100 Subject: [PATCH 35/49] better error message --- prodigy/analysis/solver/sympy_solver.py | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/prodigy/analysis/solver/sympy_solver.py b/prodigy/analysis/solver/sympy_solver.py index 1ae5baa..e476878 100644 --- a/prodigy/analysis/solver/sympy_solver.py +++ b/prodigy/analysis/solver/sympy_solver.py @@ -19,10 +19,15 @@ def solve(self, f: Distribution, g: Distribution) -> Tuple[Optional[bool], List[ s_equation = sympy.sympify(str(f - g)) if s_parameters: - solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables, dict=True, - particular=True) - # validate solutions: + try: + solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables, dict=True, particular=True) + except NotImplementedError as e: + if "no valid subset found" in str(e): + self.logger.info("%s ha no solution", s_equation) + return False, [] + + # validate solutions: # no solutions or infinitely many found. if not len(solutions) > 0: if s_equation.equals(0): From c74744d8f05916a19c9af3cfc6c5e8fb0727636d Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 12 Feb 2025 11:31:55 +0100 Subject: [PATCH 36/49] bug fix --- prodigy/analysis/solver/sympy_solver.py | 37 +++++++++++++------------ 1 file changed, 19 insertions(+), 18 deletions(-) diff --git a/prodigy/analysis/solver/sympy_solver.py b/prodigy/analysis/solver/sympy_solver.py index e476878..754a1a3 100644 --- a/prodigy/analysis/solver/sympy_solver.py +++ b/prodigy/analysis/solver/sympy_solver.py @@ -22,29 +22,30 @@ def solve(self, f: Distribution, g: Distribution) -> Tuple[Optional[bool], List[ try: solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables, dict=True, particular=True) + + # validate solutions: + # no solutions or infinitely many found. + if not len(solutions) > 0: + if s_equation.equals(0): + self.logger.debug("All parameter value combinations are valid.") + return True, [] + self.logger.debug("No solutions exist.") + return False, [] + + # at least one solution found + for sol in solutions: + for _, val in sol.items(): + if not val.free_symbols <= s_parameters: + self.logger.info("SympySolver produced the invalid result %s.", sol) + return None, [] + self.logger.debug("solutions found: %s", solutions) + return True, solutions + except NotImplementedError as e: if "no valid subset found" in str(e): self.logger.info("%s ha no solution", s_equation) return False, [] - # validate solutions: - # no solutions or infinitely many found. - if not len(solutions) > 0: - if s_equation.equals(0): - self.logger.debug("All parameter value combinations are valid.") - return True, [] - self.logger.debug("No solutions exist.") - return False, [] - - # at least one solution found - for sol in solutions: - for _, val in sol.items(): - if not val.free_symbols <= s_parameters: - self.logger.info("SympySolver produced the invalid result %s.", sol) - return None, [] - self.logger.debug("solutions found: %s", solutions) - return True, solutions - else: is_equal = s_equation.equals(0) if is_equal is None: From ea14b1f7ee66dead6dbfc352300f4a1f47f1f5f2 Mon Sep 17 00:00:00 2001 From: Lutz Klinkenberg Date: Wed, 12 Feb 2025 11:34:03 +0100 Subject: [PATCH 37/49] typo --- prodigy/analysis/solver/sympy_solver.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prodigy/analysis/solver/sympy_solver.py b/prodigy/analysis/solver/sympy_solver.py index 754a1a3..b2f07b6 100644 --- a/prodigy/analysis/solver/sympy_solver.py +++ b/prodigy/analysis/solver/sympy_solver.py @@ -43,7 +43,7 @@ def solve(self, f: Distribution, g: Distribution) -> Tuple[Optional[bool], List[ except NotImplementedError as e: if "no valid subset found" in str(e): - self.logger.info("%s ha no solution", s_equation) + self.logger.info("No solution for %s", s_equation) return False, [] else: From 9b36c043332e6662e622feca53d9aa444aede0e4 Mon Sep 17 00:00:00 2001 From: Dominik Date: Wed, 12 Feb 2025 11:44:42 +0100 Subject: [PATCH 38/49] added equivalence fail test --- .../equivalence/test_equivalence_check.py | 29 +++++++++++++++++-- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 8ca8c23..6e4f6d6 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -121,7 +121,7 @@ def test_equivalence_loop_free_benchmarks(monkeypatch, engine, file_path): @pytest.mark.parametrize( "engine", [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, - #ForwardAnalysisConfig.Engine.SYMENGINE + # ForwardAnalysisConfig.Engine.SYMENGINE ] ) @pytest.mark.parametrize( @@ -149,12 +149,35 @@ def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): assert (isinstance(prog1, Program)) assert (isinstance(prog2, Program)) - inputs = iter(["1", invariant_path]) # Simulate the input for the invariant files - monkeypatch.setattr(builtins, "input", lambda _: next(inputs)) # Select invariant file1 + monkeypatch.setattr(builtins, "input", lambda _: next(inputs)) # Select invariant file1 # Run the main program res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) assert res assert subs == [] + + +@pytest.mark.parametrize( + "engine", + [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, + # ForwardAnalysisConfig.Engine.SYMENGINE + ] +) +def test_equivalence_fail(engine): + prog1 = compile_pgcl(""" + nat x; + x := geometric(1/2); + """) + + prog2 = compile_pgcl(""" + nat x; + x := unif(1,6); + """) + + assert(isinstance(prog1, Program)) + assert(isinstance(prog2, Program)) + + res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) + assert not res From a1ca1a9e1281a9bb0c7708c3811fd196bfc20702 Mon Sep 17 00:00:00 2001 From: Dominik Date: Thu, 6 Mar 2025 15:22:58 +0100 Subject: [PATCH 39/49] fixed linting --- prodigy/analysis/equivalence/equivalence_check.py | 1 - prodigy/analysis/solver/sympy_solver.py | 3 ++- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prodigy/analysis/equivalence/equivalence_check.py b/prodigy/analysis/equivalence/equivalence_check.py index d3ced29..cf33a15 100644 --- a/prodigy/analysis/equivalence/equivalence_check.py +++ b/prodigy/analysis/equivalence/equivalence_check.py @@ -12,7 +12,6 @@ from prodigy.analysis.instructionhandler.program_info import ProgramInfo from prodigy.analysis.solver.solver_type import SolverType from prodigy.distribution.distribution import Distribution, State -from prodigy.pgcl.pgcl_operations import cav_phi from prodigy.util.color import Style from prodigy.util.logger import log_setup diff --git a/prodigy/analysis/solver/sympy_solver.py b/prodigy/analysis/solver/sympy_solver.py index b2f07b6..9274119 100644 --- a/prodigy/analysis/solver/sympy_solver.py +++ b/prodigy/analysis/solver/sympy_solver.py @@ -21,7 +21,8 @@ def solve(self, f: Distribution, g: Distribution) -> Tuple[Optional[bool], List[ if s_parameters: try: - solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables, dict=True, particular=True) + solutions = sympy.solve_undetermined_coeffs(s_equation, s_parameters, *s_variables, + dict=True, particular=True) # validate solutions: # no solutions or infinitely many found. From 890c12d3b8442425d5835b49cdce26d301f56c65 Mon Sep 17 00:00:00 2001 From: Dominik Date: Thu, 6 Mar 2025 15:49:45 +0100 Subject: [PATCH 40/49] mypy + tests --- pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl | 2 ++ pgfexamples/equivalence/loopy/random_walk.pgcl | 2 ++ prodigy/pgcl/pgcl_operations.py | 4 ++-- tests/analysis/equivalence/test_equivalence_check.py | 1 - 4 files changed, 6 insertions(+), 3 deletions(-) diff --git a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl index b2eacfb..4f645e0 100644 --- a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl +++ b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl @@ -1,3 +1,5 @@ +# skip +# FIXME compile_pgcl yields CheckFail(location=VarExpr('b1'), message='Expected numeric value, got BoolType().') # check_equality pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl bool b1 bool b2 diff --git a/pgfexamples/equivalence/loopy/random_walk.pgcl b/pgfexamples/equivalence/loopy/random_walk.pgcl index 266b329..05e13f2 100644 --- a/pgfexamples/equivalence/loopy/random_walk.pgcl +++ b/pgfexamples/equivalence/loopy/random_walk.pgcl @@ -1,3 +1,5 @@ +# skip +# CheckFail(location=BinopExpr(operator=Binop.POWER, lhs=BinopExpr(operator=Binop.MINUS, lhs=NatLitExpr(1), rhs=BinopExp...), rhs=VarExpr('c'))), rhs=RealLitExpr("1/2")), message='Expected value of type NatType(bounds=None), got RealType().' # check_equality pgfexamples/equivalence/loopy/random_walk.pgcl pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl nat s; nat c; diff --git a/prodigy/pgcl/pgcl_operations.py b/prodigy/pgcl/pgcl_operations.py index bc83cf1..a88dc97 100644 --- a/prodigy/pgcl/pgcl_operations.py +++ b/prodigy/pgcl/pgcl_operations.py @@ -25,8 +25,8 @@ def make_else_if(instructions: List[Tuple[BinopExpr, List[Instr]]]) -> IfInstr: if curr_instr is not None: curr_instr.false = [instr] curr_instr = instr - - curr_instr.false = [SkipInstr()] + if curr_instr: + curr_instr.false = [SkipInstr()] return outer_instr diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 6e4f6d6..36a61c7 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -138,7 +138,6 @@ def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): file = "\n".join(lines) invariant_path = file_path.replace("loopy/", "loopy/invariants/").replace(".pgcl", "_invariant.pgcl") - with open(invariant_path, "r") as f: inv = "\n".join(f.readlines()) From fafed5b1f863f23ccaa16825361e8746f1371d3c Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sun, 9 Mar 2025 14:09:54 +0100 Subject: [PATCH 41/49] temporarily disabled conflicting test --- tests/analysis/handlers/test_sample_handler.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/analysis/handlers/test_sample_handler.py b/tests/analysis/handlers/test_sample_handler.py index 5324a1d..0594f1f 100644 --- a/tests/analysis/handlers/test_sample_handler.py +++ b/tests/analysis/handlers/test_sample_handler.py @@ -7,7 +7,7 @@ from prodigy.distribution.generating_function import SympyPGF from prodigy.distribution.symengine_distribution import SymenginePGF - +@pytest.mark.skip("FIXME This test fails only if one executes all tests at once, not if one executes it alone.") @pytest.mark.parametrize('engine,factory', [(ForwardAnalysisConfig.Engine.SYMPY, SympyPGF), (ForwardAnalysisConfig.Engine.GINAC, ProdigyPGF), From 00bb2345352ceac58c7ed69b4a48c7d702d1ffcd Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sun, 9 Mar 2025 14:55:35 +0100 Subject: [PATCH 42/49] introduced test order to fix error #64 --- pyproject.toml | 1 + tests/analysis/equivalence/test_equivalence_check.py | 4 +++- tests/analysis/handlers/test_sample_handler.py | 1 - 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 3234d23..0bbc04d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -45,6 +45,7 @@ yapf = "^0.30.0" jinja2 = "3.1.4" rope = "^0.17.0" pytest-cov = "^2.9.0" +pytest-ordering = "^0.6" hypothesis = "^5.18.0" [tool.poetry.scripts] diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 36a61c7..8848e82 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -117,7 +117,6 @@ def test_equivalence_loop_free_benchmarks(monkeypatch, engine, file_path): assert res assert subs == [] - @pytest.mark.parametrize( "engine", [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, @@ -129,6 +128,9 @@ def test_equivalence_loop_free_benchmarks(monkeypatch, engine, file_path): [y for x in os.walk("pgfexamples/equivalence/loopy") for y in glob(os.path.join(x[0], '*.pgcl')) if not "invariants" in y] ) +# This test apparently has some side-effect which fails other tests (cf. #64), if it is executed last +# this problem does not occur +@pytest.mark def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): # Read the body of the program files with open(file_path, "r") as f: diff --git a/tests/analysis/handlers/test_sample_handler.py b/tests/analysis/handlers/test_sample_handler.py index 0594f1f..e1ebe29 100644 --- a/tests/analysis/handlers/test_sample_handler.py +++ b/tests/analysis/handlers/test_sample_handler.py @@ -7,7 +7,6 @@ from prodigy.distribution.generating_function import SympyPGF from prodigy.distribution.symengine_distribution import SymenginePGF -@pytest.mark.skip("FIXME This test fails only if one executes all tests at once, not if one executes it alone.") @pytest.mark.parametrize('engine,factory', [(ForwardAnalysisConfig.Engine.SYMPY, SympyPGF), (ForwardAnalysisConfig.Engine.GINAC, ProdigyPGF), From 6d453429fe79033baefefedd8385205013acb29f Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sun, 9 Mar 2025 15:01:36 +0100 Subject: [PATCH 43/49] typo --- tests/analysis/equivalence/test_equivalence_check.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 8848e82..47f8535 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -130,7 +130,7 @@ def test_equivalence_loop_free_benchmarks(monkeypatch, engine, file_path): ) # This test apparently has some side-effect which fails other tests (cf. #64), if it is executed last # this problem does not occur -@pytest.mark +@pytest.mark.last def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): # Read the body of the program files with open(file_path, "r") as f: From 0bf3e43fe4d4799ac02f7c1dbd338c23a9584476 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Mon, 10 Mar 2025 14:36:05 +0100 Subject: [PATCH 44/49] Benchmark script can now handle multiple invariant files, removed todos, adjusted readme and tests --- benchmark_comparison.py | 12 ++++++++---- pgfexamples/README.md | 3 +++ ...e_inv_outer.pgcl => nested_while_invariant1.pgcl} | 0 ...e_inv_inner.pgcl => nested_while_invariant2.pgcl} | 0 ...rst_inv.pgcl => sequential_loops_invariant1.pgcl} | 0 ...ond_inv.pgcl => sequential_loops_invariant2.pgcl} | 0 pgfexamples/equivalence/loopy/nested_while.pgcl | 2 +- pgfexamples/equivalence/loopy/sequential_loops.pgcl | 4 +--- prodigy/analysis/instructionhandler/while_handler.py | 2 -- tests/analysis/equivalence/test_equivalence_check.py | 5 +++++ 10 files changed, 18 insertions(+), 10 deletions(-) rename pgfexamples/equivalence/loopy/invariants/{nested_while_inv_outer.pgcl => nested_while_invariant1.pgcl} (100%) rename pgfexamples/equivalence/loopy/invariants/{nested_while_inv_inner.pgcl => nested_while_invariant2.pgcl} (100%) rename pgfexamples/equivalence/loopy/invariants/{sequential_loops_first_inv.pgcl => sequential_loops_invariant1.pgcl} (100%) rename pgfexamples/equivalence/loopy/invariants/{sequential_loops_second_inv.pgcl => sequential_loops_invariant2.pgcl} (100%) diff --git a/benchmark_comparison.py b/benchmark_comparison.py index 67232a2..df78a20 100755 --- a/benchmark_comparison.py +++ b/benchmark_comparison.py @@ -263,10 +263,9 @@ def benchmark(config: Configuration): continue output = "" - # Execute the program cmd = ["python", "prodigy/cli.py", "--engine", engine, *instructions] - + print(bytes.decode(inputs)) try: output = subprocess.check_output(cmd, timeout=config.timeout, input=inputs).decode() except TimeoutExpired as e: @@ -378,8 +377,13 @@ def obtain_inputs(instructions: list[str]) -> bytes: other_file = instructions[2] input_cmd = b"" if method == "check_equality" and ("loopy" in other_file or "template_parameter_synthesis"): - # Select invariant file for loopy programs - input_cmd = b"1\n" + str.encode(other_file + "\n") + if other_file.endswith("1.pgcl"): + # We have multiple invariants + input_cmd = str.encode("".join("1\n" + inv_file + "\n" for inv_file in + list(sorted(glob(other_file.replace("1.pgcl", "*")))))) + else: + # Select invariant file for loopy programs + input_cmd = b"1\n" + str.encode(other_file + "\n") return input_cmd def capture_output(output: list[str], cmd: list[str], file: str) -> Run: diff --git a/pgfexamples/README.md b/pgfexamples/README.md index 7d44df4..92d563d 100644 --- a/pgfexamples/README.md +++ b/pgfexamples/README.md @@ -47,4 +47,7 @@ pgfexamples/ * In `pgfexamples/equivalence/loopy` and `pgfexamples/template_parameter_synthesis` the files are named `file_name.pgcl` in the main folder and their corresponding invariants with `file_name_invariant.pgcl` in the invariants folder + * If there are multiple invariant files for one program, e.g. for a nested loop, the invariants are to be marked + with numbers indicating the order they should be used (i.e. the invariant for the outer-most while loop has number + 1 and so on) * Invariants and second programs are to be marked with `skip` \ No newline at end of file diff --git a/pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl similarity index 100% rename from pgfexamples/equivalence/loopy/invariants/nested_while_inv_outer.pgcl rename to pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl diff --git a/pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl b/pgfexamples/equivalence/loopy/invariants/nested_while_invariant2.pgcl similarity index 100% rename from pgfexamples/equivalence/loopy/invariants/nested_while_inv_inner.pgcl rename to pgfexamples/equivalence/loopy/invariants/nested_while_invariant2.pgcl diff --git a/pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl similarity index 100% rename from pgfexamples/equivalence/loopy/invariants/sequential_loops_first_inv.pgcl rename to pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl diff --git a/pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl b/pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant2.pgcl similarity index 100% rename from pgfexamples/equivalence/loopy/invariants/sequential_loops_second_inv.pgcl rename to pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant2.pgcl diff --git a/pgfexamples/equivalence/loopy/nested_while.pgcl b/pgfexamples/equivalence/loopy/nested_while.pgcl index 9835ce2..37ae1b8 100644 --- a/pgfexamples/equivalence/loopy/nested_while.pgcl +++ b/pgfexamples/equivalence/loopy/nested_while.pgcl @@ -1,4 +1,4 @@ -# skip +# check_equality pgfexamples/equivalence/loopy/nested_while.pgcl pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl # TODO how to do this with the CLI nat x; nat y; diff --git a/pgfexamples/equivalence/loopy/sequential_loops.pgcl b/pgfexamples/equivalence/loopy/sequential_loops.pgcl index b2c3c00..1867d73 100644 --- a/pgfexamples/equivalence/loopy/sequential_loops.pgcl +++ b/pgfexamples/equivalence/loopy/sequential_loops.pgcl @@ -1,6 +1,4 @@ -# skip -# TODO how to do this with CLI? -# check_equality pgfexamples/equivalence/loopy/sequential_loops.pgcl pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant.pgcl +# check_equality pgfexamples/equivalence/loopy/sequential_loops.pgcl pgfexamples/equivalence/loopy/invariants/sequential_loops_invariant1.pgcl nat c; nat m; nat n; diff --git a/prodigy/analysis/instructionhandler/while_handler.py b/prodigy/analysis/instructionhandler/while_handler.py index 4998f21..e38f178 100644 --- a/prodigy/analysis/instructionhandler/while_handler.py +++ b/prodigy/analysis/instructionhandler/while_handler.py @@ -209,7 +209,6 @@ def _evt_invariant( solutions.append(candidate) if len(solutions) > 0: print(f"All solutions: {solutions}") - # TODO use a solution to compute the final distribution. logger.info("Using the first solution to continue.") sol_dist = config.factory.from_expr( sympy.S(str(evt_inv - evt_inv.filter(instruction.cond))).subs(solutions[0])) @@ -295,7 +294,6 @@ def compute( if user_choice == "5": return WhileHandler._evt_invariant(instruction, prog_info, distribution, error_prob, config, analyzer) if user_choice == "6": - # TODO include phi step here? return WhileHandler._evt_invariant_synthesis(instruction, prog_info, distribution, error_prob, config, analyzer) if user_choice == "q": diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 47f8535..9699f71 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -1,6 +1,8 @@ import builtins import os from glob import glob +from os.path import isfile + import pytest import sympy from probably.pgcl.ast import Program @@ -140,6 +142,9 @@ def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): file = "\n".join(lines) invariant_path = file_path.replace("loopy/", "loopy/invariants/").replace(".pgcl", "_invariant.pgcl") + if not isfile(invariant_path): + pytest.skip("File has multiple invariants") + with open(invariant_path, "r") as f: inv = "\n".join(f.readlines()) From f58b3483a8f87e279dda8a13eb3ea2336c2afbcb Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Mon, 10 Mar 2025 14:38:49 +0100 Subject: [PATCH 45/49] #63 resolved the issue with bit_flip_conditioning --- pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl index 4f645e0..e25bd8c 100644 --- a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl +++ b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl @@ -1,5 +1,3 @@ -# skip -# FIXME compile_pgcl yields CheckFail(location=VarExpr('b1'), message='Expected numeric value, got BoolType().') # check_equality pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl pgfexamples/equivalence/loopy/invariants/bit_flip_conditioning_invariant.pgcl bool b1 bool b2 @@ -8,7 +6,7 @@ bool b4 nat i nat temp -while (not ((b1 = 0) & (b2 = 0))) { +while (b1 || b2) { b1 := bernoulli(1/2) b2 := bernoulli(1/2) observe( (b1 = 0 & b3 = 0) || (b1 = 1 & b3 = 1) || (b2 = 0 & b4 = 0) || (b2 = 1 & b4 = 1) ) From a78f30c102b5d93ef5ba9ff716579960bae98f9b Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sat, 15 Mar 2025 10:07:48 +0100 Subject: [PATCH 46/49] changed compile -> parse --- pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl | 2 +- tests/analysis/equivalence/test_equivalence_check.py | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl index e25bd8c..51de045 100644 --- a/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl +++ b/pgfexamples/equivalence/loopy/bit_flip_conditioning.pgcl @@ -6,7 +6,7 @@ bool b4 nat i nat temp -while (b1 || b2) { +while (b1=1 || b2=1) { b1 := bernoulli(1/2) b2 := bernoulli(1/2) observe( (b1 = 0 & b3 = 0) || (b1 = 1 & b3 = 1) || (b2 = 0 & b4 = 0) || (b2 = 1 & b4 = 1) ) diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 9699f71..2203a6e 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -5,6 +5,7 @@ import pytest import sympy +from probably.pgcl import parse_pgcl from probably.pgcl.ast import Program from probably.pgcl.compiler import compile_pgcl @@ -99,7 +100,7 @@ def test_equivalence_check_parameter(engine): [y for x in os.walk("pgfexamples/equivalence/loop_free") for y in glob(os.path.join(x[0], '*.pgcl')) if not y.endswith('2.pgcl')] ) -def test_equivalence_loop_free_benchmarks(monkeypatch, engine, file_path): +def test_equivalence_loop_free_benchmarks(engine, file_path): # Read the body of the program files with open(file_path, "r") as f: file = "\n".join(f.readlines()) @@ -149,8 +150,8 @@ def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): inv = "\n".join(f.readlines()) # Compile them to a program object - prog1 = compile_pgcl(file) - prog2 = compile_pgcl(inv) + prog1 = parse_pgcl(file) + prog2 = parse_pgcl(inv) assert (isinstance(prog1, Program)) assert (isinstance(prog2, Program)) From 020e28734e562a5e1a7781b85d0669cb8cc77c82 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sat, 15 Mar 2025 10:14:41 +0100 Subject: [PATCH 47/49] resolved todo --- pgfexamples/equivalence/loopy/nested_while.pgcl | 1 - pgfexamples/equivalence/loopy/random_walk.pgcl | 2 -- 2 files changed, 3 deletions(-) diff --git a/pgfexamples/equivalence/loopy/nested_while.pgcl b/pgfexamples/equivalence/loopy/nested_while.pgcl index 37ae1b8..17928c5 100644 --- a/pgfexamples/equivalence/loopy/nested_while.pgcl +++ b/pgfexamples/equivalence/loopy/nested_while.pgcl @@ -1,5 +1,4 @@ # check_equality pgfexamples/equivalence/loopy/nested_while.pgcl pgfexamples/equivalence/loopy/invariants/nested_while_invariant1.pgcl -# TODO how to do this with the CLI nat x; nat y; nat c; diff --git a/pgfexamples/equivalence/loopy/random_walk.pgcl b/pgfexamples/equivalence/loopy/random_walk.pgcl index 05e13f2..266b329 100644 --- a/pgfexamples/equivalence/loopy/random_walk.pgcl +++ b/pgfexamples/equivalence/loopy/random_walk.pgcl @@ -1,5 +1,3 @@ -# skip -# CheckFail(location=BinopExpr(operator=Binop.POWER, lhs=BinopExpr(operator=Binop.MINUS, lhs=NatLitExpr(1), rhs=BinopExp...), rhs=VarExpr('c'))), rhs=RealLitExpr("1/2")), message='Expected value of type NatType(bounds=None), got RealType().' # check_equality pgfexamples/equivalence/loopy/random_walk.pgcl pgfexamples/equivalence/loopy/invariants/random_walk_invariant.pgcl nat s; nat c; From 479ff035b575bd06a054849ebf0cface81ae0106 Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sat, 15 Mar 2025 10:19:29 +0100 Subject: [PATCH 48/49] ivars -> independent_vars_analysis --- prodigy/cli.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/prodigy/cli.py b/prodigy/cli.py index 44e1fd2..022c1d2 100644 --- a/prodigy/cli.py +++ b/prodigy/cli.py @@ -27,7 +27,7 @@ from prodigy.analysis.exceptions import VerificationError from prodigy.analysis.instructionhandler.program_info import ProgramInfo from prodigy.analysis.solver.solver_type import SolverType -from prodigy.analysis.independence.independence import independent_vars as ivars +from prodigy.analysis.independence.independence import independent_vars as independent_vars_analysis from prodigy.distribution.distribution import State from prodigy.util.color import Style from prodigy.util.logger import log_setup @@ -194,7 +194,7 @@ def independent_vars(ctx, program_file: IO, compute_exact: bool): raise ValueError(f"Could not compile the Program. {prog}") start = time.perf_counter() - indep_rel: Set[frozenset[Var]] = ivars(prog) #, program_file, compute_exact) + indep_rel: Set[frozenset[Var]] = independent_vars_analysis(prog) #, program_file, compute_exact) stop = time.perf_counter() print(Style.OKBLUE + "Under-approximation: \t" + str(indep_rel) + Style.RESET) From 90f1f697bf1279a8ba9e09112e7af299485abaca Mon Sep 17 00:00:00 2001 From: dominikgeissler Date: Sat, 15 Mar 2025 11:01:21 +0100 Subject: [PATCH 49/49] investigation into failing tests --- tests/analysis/equivalence/test_equivalence_check.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/tests/analysis/equivalence/test_equivalence_check.py b/tests/analysis/equivalence/test_equivalence_check.py index 2203a6e..136ae46 100644 --- a/tests/analysis/equivalence/test_equivalence_check.py +++ b/tests/analysis/equivalence/test_equivalence_check.py @@ -122,7 +122,7 @@ def test_equivalence_loop_free_benchmarks(engine, file_path): @pytest.mark.parametrize( "engine", - [ForwardAnalysisConfig.Engine.GINAC, ForwardAnalysisConfig.Engine.SYMPY, + [ ForwardAnalysisConfig.Engine.GINAC,ForwardAnalysisConfig.Engine.SYMPY, # ForwardAnalysisConfig.Engine.SYMENGINE ] ) @@ -133,7 +133,7 @@ def test_equivalence_loop_free_benchmarks(engine, file_path): ) # This test apparently has some side-effect which fails other tests (cf. #64), if it is executed last # this problem does not occur -@pytest.mark.last +# FIXME this test has some effect on GINAC, when removing GINAC from the engine list, all tests pass def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): # Read the body of the program files with open(file_path, "r") as f: @@ -158,10 +158,11 @@ def test_equivalence_loopy_benchmarks(monkeypatch, engine, file_path): inputs = iter(["1", invariant_path]) # Simulate the input for the invariant files - monkeypatch.setattr(builtins, "input", lambda _: next(inputs)) # Select invariant file1 + with monkeypatch.context() as m: + m.setattr("builtins.input", lambda _: next(inputs)) # Select invariant file1 + # Run the main program + res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) - # Run the main program - res, subs = check_equivalence(prog1, prog2, ForwardAnalysisConfig(engine=engine), compute_semantics) assert res assert subs == []