More control over the termination of quantification elimination

[jgroote]

Issue migrated from trac ticket # 954

component: PBES Library | priority: major

2012-01-27 15:28:29: @twillems created the issue

---

When confronted with a PBES containing quantifications over infinite data sorts such as natural numbers, it would be helpful if the termination of quantifier elimination (offered by pbesrewr) could be assisted by a user-specified limit (such as a maximal number of 'unfoldings' or a maximal amount of time to be spent on eliminating a quantifier).

This would enable one to still simplify right-hand side expressions of PBES equations such as:

pbes

nu X(i:Nat) #  (exists n:Nat. val(n ## 3 || n 2) && val(n > 0)) || (forall k: Nat. val(k >= i)> X(k) ) ;

init X(0);

which may now spend all its time in simplifying the right-hand side argument of the disjunction.

[jgroote]

2012-08-24 07:05:07:

[jgroote]

2012-08-24 07:05:07: commented

---

Milestone To be decided deleted

[jgroote]

2017-05-04 14:52:31: @wiegerw