Skip to Content.
Sympa Menu

k-user - Re: [[K-user] ] state space search in KCC 3.4

k-user AT lists.cs.illinois.edu

Subject: K-user mailing list

List archive

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


Chronological Thread 
  • From: Jan Tušil <jenda.tusil AT gmail.com>
  • To: "k-user AT lists.cs.illinois.edu" <k-user AT lists.cs.illinois.edu>
  • Subject: Re: [[K-user] ] state space search in KCC 3.4
  • Date: Wed, 14 Mar 2018 23:54:00 +0100
  • Authentication-results: illinois.edu; spf=pass smtp.mailfrom=jenda.tusil AT gmail.com; dkim=pass header.d=gmail.com header.s=20161025; dmarc=pass header.from=gmail.com

Maybe try sending the generated config file, if there is one.

2018-03-14 23:22 GMT+01:00 Christos Kloukinas <c.kloukinas AT gmail.com>:

No idea really but maybe your main should be:

int main(int argc, char** argv)

instead of:

int main(void)

?

A very wild guess...


Christos


On 13/03/2018 12:27, dexter wrote:

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





--
"If I have seen further, it is by standing on the shoulders of giants." (Sir Isaac Newton)



Archive powered by MHonArc 2.6.19.

Top of Page