Between pattern (Test case: tmp_betweenand01.cfr)

[RaoMukkamala]

Checks

1. test case is ok ? Yes
2. Compiles ? Yes
3. De-sugars correctly ? yes
4. Compiles in Alloy ? Yes
5. Instances in alloy are ok? no instance found.

Model:

a   xor b    c    d    e    [always c between d and e ]    [sometime d]    [sometime c]    [sometime e] assert[always c between d and e]

When tested the following alloy code generated for the above model, it fails to generate a sample instance. Interstingly, if I comment [sometime e] constraint, it generates an instance without e. This case is similar to after and until pattern, where it also fails to generate a instance with suitable start and end scopes.

/*
All clafers: 5 | Abstract: 0 | Concrete: 5 | References: 0
Constraints: 5
Goals: 0
Global scope: 1..1
Can skip resolver: yes
*/

open util/ordering[Time]
pred show {}
run show for 10

sig Time {loop: lone Time}
fact Loop {loop in last->Time}
fun timeLoop: Time -> Time { Time <: next + loop }

one sig root
{ r_c0_a : c0_a -> Time }
{ all t : Time | one r_c0_a.t }

sig c0_a
{ r_c0_b : c0_b -> Time }
{ all t : Time | one r_c0_b.t }

sig c0_b
{ r_c0_c : c0_c -> Time
, r_c0_d : c0_d -> Time
, r_c0_e : c0_e -> Time }
{ all t : Time | lone r_c0_c.t && lone r_c0_d.t && lone r_c0_e.t
  all t : Time | let children = (r_c0_c.t + r_c0_d.t + r_c0_e.t) | one children
  let local_next = (this.(c0_a.@r_c0_b)) <: next  | one t : Time | one t <: local_next and no local_next :> t and 
  (some loop and all t':t.*timeLoop | (((some this.@r_c0_d.t') && (no this.@r_c0_e.t')) && ((some t'':t'.*timeLoop | some this.@r_c0_e.t''))) => ((some t'':t'.*timeLoop | some this.@r_c0_e.t'' and ( all t''':t'.*timeLoop & ^timeLoop.t''|some this.@r_c0_c.t'''))))
  let local_next = (this.(c0_a.@r_c0_b)) <: next  | one t : Time | one t <: local_next and no local_next :> t and 
  (some t':t.*timeLoop | some this.@r_c0_d.t')
  let local_next = (this.(c0_a.@r_c0_b)) <: next  | one t : Time | one t <: local_next and no local_next :> t and 
  (some t':t.*timeLoop | some this.@r_c0_c.t')
  let local_next = (this.(c0_a.@r_c0_b)) <: next  | one t : Time | one t <: local_next and no local_next :> t and 
  (some t':t.*timeLoop | some this.@r_c0_e.t') }

sig c0_c
{}
{ all t : Time | one r_c0_c.t }

sig c0_d
{}
{ all t : Time | one r_c0_d.t }

sig c0_e
{}
{ all t : Time | one r_c0_e.t }

assert assertOnLine_12 { one t : first <: Time | (some loop and all t':t.*timeLoop | (((some (@r_c0_a.t'.@r_c0_b.t').@r_c0_d.t') && (no (@r_c0_a.t'.@r_c0_b.t').@r_c0_e.t')) && ((some t'':t'.*timeLoop | some (@r_c0_a.t''.@r_c0_b.t'').@r_c0_e.t''))) => ((some t'':t'.*timeLoop | some (@r_c0_a.t''.@r_c0_b.t'').@r_c0_e.t'' and ( all t''':t'.*timeLoop & ^timeLoop.t''|some (@r_c0_a.t'''.@r_c0_b.t''').@r_c0_c.t''')))) }
check assertOnLine_12 for 0

[juodaspaulius]

Current version generates a trace which satisfies constraints. But among first many I could not find a trace that would have c sandwiched between d and e. e always appears in the first snapshot, but not later...

[wasowski]

@RaoMukkamala perhaps we could have a test-case that tries to more directly force a later occurrence of c?

[juodaspaulius]

I tried to use initially to force initial d to show up. But that didn't work. Alloy simply wasn't returning any instances.

Since always-between pattern use G(a U b) expression, I rewrote this model to simpler version:

final xor b 
  d 
  e 
  [G ( d U e) ]

Compiled to alloy and ran through analyzer. Unfortunately Alloy did not give any instances again. But there is a definitely a valid traces in here such as a simple:

b      b    b
  e     e     e .........

If xor is removed, the analyzer does find trace, which have snapshots with d&e appearing together:

b
     d
     e

Compiled alloy is:

/*
All clafers: 3 | Abstract: 0 | Concrete: 3 | Reference: 0
Constraints: 1
Goals: 0
Global scope: 1..1
Can skip name resolver: yes
*/

open util/ordering[Time]
pred show {}
run show for 10

sig Time {loop: lone Time}
fact Loop { #loop > 0 && loop in last->Time}
fun timeLoop: Time -> Time { Time <: next + loop }
fun local_first [rel: univ->univ->Time, parentSet: univ, child: univ] : Time {
  {t: Time | t in (child.(parentSet.rel)) and no ((child.(parentSet.rel)) <: next) :> t }
}

one sig root
{ r_c0_b : one c0_b }

sig c0_b
{ r_c0_d : c0_d -> Time 
, r_c0_e : c0_e -> Time }
{ one @r_c0_b.this
  all t : Time | lone r_c0_d.t &&   lone r_c0_e.t
-- this is the xor line:
  all t : Time | one (r_c0_d.t + r_c0_e.t)
  one t: Time <: first | (all t':t.*timeLoop | (some t'':t'.*timeLoop | some this.@r_c0_e.t'' and ( all t''':t'.*timeLoop & ^timeLoop.t''|some this.@r_c0_d.t'''))) 
}

sig c0_d
{}
{ lone local_first[r_c0_d, c0_b, this] && lone r_c0_d.Time.this }

sig c0_e
{}
{ lone local_first[r_c0_e, c0_b, this] && lone r_c0_e.Time.this }

Looks like there might be a problem with U encoding when used in the context of G modality, but can't think of why?...

For reference, A. Cunha's original encodings are:

EDIT: Removed c which is not needed and added comments in alloy