Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

unexpected behaviour with set comprehension #1794

Open
gjveltink opened this issue Dec 6, 2024 · 3 comments
Open

unexpected behaviour with set comprehension #1794

gjveltink opened this issue Dec 6, 2024 · 3 comments

Comments

@gjveltink
Copy link

Either my understanding of set comprehension in mCRL2 is fundamentally flawed or there is something funky with its implementation.
I have tried to experiment with the definition of the prime numbers as given on the web site in the section "Data Specifications".
{ n: Pos | n > 1 && forall m, m': Pos . (m > 1 && m' > 1) => n != m * m' }

I expected to be able to use the term rewriter to test the primeness of numbers like:
1 in { n: Pos | n > 1 && forall m, m': Pos . (m > 1 && m' > 1) => n != m * m' }
This results in "false" es expected.

However, testing primeness of "2" does not result in "true", instead it results in:
forall m,m': Pos. 1 < m && 1 < m' => !(2 == m * m')

Testing "4" results in: "false" as expected.
Testing "6" results in: "false" as expected.
Testing "8" results in: "false" as expected.

However, testing "9" results in:
forall m,m': Pos. 1 < m && 1 < m' => !(9 == m * m')

and Testing "10" results in:
forall m,m': Pos. 1 < m && 1 < m' => !(10 == m * m')

I cannot see the pattern here!

To be able to quickly test a series of values I constructed the following small process specification.
Please help me, I am confused.

%
% A simple example to demonstrate the use of quantifiers
%

map
  	primes: Set(Pos);

eqn
	primes = { n: Pos | n > 1 && forall m, m': Pos . (m > 1 && m' > 1) => n != m * m' };

%------------------------------------------

act 
	isPrime: Pos # Bool;

proc
	ShowPrimes = ShowPrimes(1);
	ShowPrimes(p : Pos) = (p < 15) -> isPrime(p, p in primes) . ShowPrimes(p + 1);	

init
	ShowPrimes;
@jgroote
Copy link
Member

jgroote commented Dec 7, 2024 via email

@gjveltink
Copy link
Author

Hi Jan Friso,

Many thanks for your rapid reply!

I have been able to successfully reproduce your results.
Unfortunately, this will not work within the IDE, which is where my students normally spend most of their time.

But I get the point, we have to try to manually prune the search space of the quantifiers such that the tool is more likely to find the solution.
Do I understand the explanation of the QBOUND correctly, that with the default setting each quantifier will be tried for the first 10 values, in this case n = 2..11, m = 2..11, m' = 2..11?

I will check whether I can come up with a more restrictive definition of primes, such that a larger number of values can be found with the default settings.

Cheers!

Gert

@gjveltink
Copy link
Author

OK, I now have done some experiments.

primes = { n: Pos | n > 1 && forall m, m': Pos . (n>m && m > 1 && n>m' && m'>1) => n != m * m' };
Needs -Q144 for the given example. I assume that is 12 * 12, or the equivalent of m = 0..11, m' = 0..11.

I have been able to improve the value of -Q down to -Q33, but not the legibility, unfortunately! ;-)
primes = { n: Pos | n > 1 && forall m, m': Pos. (m > 1 && m' > 1 && m <= (n div 2) && m' <= (n div 2) && m <= m' && m * m' <= n) => n != m * m' };

One small final request.
Would it be possible to set the default value for -Q to 100 or maybe add -Q as a setting to the IDE?

Cheers!

Gert

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gjveltink @jgroote