No counterexample found issue

I have this model, basically services store a list of -> request id. I created a request which isn’t in the list, so I would expect no change to the buffer that is used to store the request hits. But I tested it against s.buffer' = s.buffer + ->, I would expect a counterexample, but none is found.

sig Id, Name {}

abstract sig Request {
	id : Id,	
	name : Name

abstract sig Service { 
	var list : Name -> set Id 

sig Service1 extends Service      { 
	-- store hits in buffer
	var buffer : Name -> set Id 

sig HitMissRequest extends Request {} { 
	no a : Service1 | name -> id in a.list

pred Process [r : Request, s : Service] {
	isHit[r, s] and 	
       -- since it's miss s.buffer' should equal to s.buffer only								
	s.buffer' = s.buffer + ->

pred isHit [r : Request, s : Service] { -> in s.list

assert MissRequest {
	all r : HitMissRequest, s : Service1 |
		Process[r, s] implies
			s.buffer' = s.buffer + ->

check MissRequest

no Counterexample found, no sure why.

There is no counterexample because Process[r,s] is always false when r is a HitMissRequest, hence the implication is true.
Maybe you had in mind a different specification for Process, namely one that keeps the buffer the same if the request does not satisfy isHit. Something as follows:

pred Process [r : Request, s : Service] {
	isHit[r, s] implies s.buffer' = s.buffer + ->
	else s.buffer' = s.buffer

With this specification you will get a counterexample.

1 Like

Thank you so much Alcino! I looked up implication true table, False → True and False → False both result in True. This issue is tricky for me to figure out. I have changed pred according to your suggestion. It worked!!