# No counterexample found issue

**URL:** <https://alloytools.discourse.group/t/no-counterexample-found-issue/317>\
**Category:** Questions\
**Created:** [December 30, 2022, 5:42am UTC](https://alloytools.discourse.group/t/no-counterexample-found-issue/317 "2022-12-30T05:42:03Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![victor](https://avatars.discourse-cdn.com/v4/letter/v/3e96dc/32.png) [@victor](https://alloytools.discourse.group/u/victor)\
**Post date:** [December 30, 2022, 5:42am UTC](https://alloytools.discourse.group/t/no-counterexample-found-issue/317/1 "2022-12-30T05:42:03Z")

</div>

I have this model, basically services store a list of `request.name -> 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 + r.name -> r.id`, I would expect a counterexample, but none is found.

```auto
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 + r.name -> r.id
}

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

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

check MissRequest

```

no Counterexample found, no sure why.

---

<div class="post-metadata">

**Author:** ![alcino](https://yyz2.discourse-cdn.com/free1/user_avatar/alloytools.discourse.group/alcino/32/25_2.png) [@alcino](https://alloytools.discourse.group/u/alcino)\
**Post date:** [December 30, 2022, 5:07pm UTC](https://alloytools.discourse.group/t/no-counterexample-found-issue/317/2 "2022-12-30T17:07:15Z")

</div>

Hi,  
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:

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

```

With this specification you will get a counterexample.  
Best,  
Alcino

---

<div class="post-metadata">

**Author:** ![victor](https://avatars.discourse-cdn.com/v4/letter/v/3e96dc/32.png) [@victor](https://alloytools.discourse.group/u/victor)\
**Post date:** [December 30, 2022, 10:48pm UTC](https://alloytools.discourse.group/t/no-counterexample-found-issue/317/3 "2022-12-30T22:48:38Z")

</div>

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!!