k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

[[K-user] ] state space search in KCC 3.4

From: dexter <qjq793437528 AT 163.com>
To: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
Subject: [[K-user] ] state space search in KCC 3.4
Date: Tue, 13 Mar 2018 20:27:48 +0800
Authentication-results: illinois.edu; spf=pass smtp.mailfrom=qjq793437528 AT 163.com; dkim=pass header.d=163.com header.s=s110527; dmarc=none
Importance: normal

Hello!

I'm trying to use the state space search in KCC. however when i run some very simple program like :

int r = 0 ;

int f(int x)
{

return (r = x) ;

}

int main(void)
{ f(1) ;
// f(1) + f(2) ;
return 0 ;

}

Obviously, this program is correct with no non-determinism, when i run the a.out with option --SEARCH=1 ,it shows the only one solution and this solution is the program got stuck . what's wrong with this? how can i fix it? thanks very much.

best

[[K-user] ] state space search in KCC 3.4, dexter, 03/13/2018
- Re: [[K-user] ] state space search in KCC 3.4, Christos Kloukinas, 03/14/2018
  - Re: [[K-user] ] state space search in KCC 3.4, Jan Tušil, 03/14/2018
- Re: [[K-user] ] state space search in KCC 3.4, Tim Swan, 03/15/2018