Constraint language not fully supported in assertions

[RaoMukkamala]

The constraint language is not fully supported in assertions.

Test case:
a ?
  xor b 1
    c ?
      d ?
    [never d after c ]

assert [all a1 : a | all b1 : a1.b | never b1.d after b1.c]

In the above test case the assertion fails with the following error message Error message:

clafer: AlloyLtl.genPExp': No pattern match for IClaferId {_modName = "", _sident = "a1", _isTop = True, _binding = Nothing}
[Finished in 0.0s with exit code 1]
[cmd: ['/home/clafertools/.config/sublime-text-3/Packages/Clafer Tools/clafer', '/home/clafertools/behavioral-0.4.0/clafer/test/positive/tmp_after01.cfr', '-m=alloyltl', '-m=clafer', '-m=html', '--add-comments', '--self-contained']]
[dir: /home/clafertools/behavioral-0.4.0/clafer/test/positive]
[path: .:/opt/ghc/7.8.3/bin:/opt/cabal/1.20/bin:/home/clafertools/.cabal/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games]

[mantkiew]

I tried fixing that (see commit) but I am getting some weird Alloy error about higher-order quantification needed. I don't know Alloy well enough to fix that. @juodaspaulius, please give it a shot. Also, see the test case, which is a temporal version of static test case. The static one works well.

[juodaspaulius]

I was also getting high-order quantification error. This is a snippet that the tool generates for the temporal test case:

one sig root
{ r_c0_A : c0_A -> State }
{ one t: State <: first | 
  (infinite and all t':t.*next | all  c : (**@**r_c0_A.t'.@r_c0_B.t').@r_c0_C.t' | one c.@r_c0_D.t')
  one t: State <: first | 
  (some t':t.*next | some (@r_c0_A.t'.@r_c0_B.t').@r_c0_C.t') }

If I remove "@" marked with stars then it works.

Issue is that root clafer is introduced in generator stage, not desugaring. So path from root to A does not get the necessary "this". In other words, in root level constraint reference to A should be resolved to "this.A" - same as in subclafers.

See the last constraint in this desugared test case:

0 .. * c0_A 0 .. * {
  0 .. * c0_B 0 .. * {
    0 .. * c0_C 0 .. * {
      0 .. * c0_D 0 .. 1 {
        }
      }
    [G one this . c0_C . c0_D]
  }
  [G (all c : this . c0_B . c0_C | one c . c0_D)] 
}
[G (all c : c0_A . c0_B . c0_C | one c . c0_D)] [F some c0_A . c0_B . c0_C]assert [G (all c : c0_A . c0_B . c0_C | some c . c0_D)]

[wasowski]

This looks quite complex; I will try to understand this for our meeting today.

Notes:

1. I seem to be unable to run the static test case through the Alloy (Non LTL) generator. The tool always uses AlloyLtL.
2. Do we have the same problem on the structural generator?
3. I have read up on the semantics of '@' in Alloy and I am less and less convinced why we use it at all. I am analyzing the constraints in this example, and it does not seem that '@' is needed anywhere, while it introduces the root problem. It would be nice to recall why @ appears at all in these encodings of clafer.