DistCompiler / pgo

PGo is a source to source compiler from Modular PlusCal specs into Go programs.
https://distcompiler.github.io/
Apache License 2.0
173 stars 13 forks source link

Wrong parsing of expression #84

Closed minhnhdo closed 6 years ago

minhnhdo commented 6 years ago

The following PlusCal spec is parsed incorrectly.

 ---- MODULE Test ----
 EXTENDS Sequences, Integers
 (* --algorithm Test {
     variables set = {2,4,6};
     {
         print \A x \in set,y \in (1)..(3) : (((x)+(y))%(2))=(1)
     }
 }
 *)
 ====

The compiled Go program is as follows.

package main

import (
    "fmt"
)

func init() {
}

func main() {
    set := []int{2, 4, 6}
    exists := false
    tmpRange := make([]int, 3-1+1)
    for i := 1; i <= 3; i++ {
        tmpRange[i-1] = i
    }
    for _, x := range set {
        for _, y := range tmpRange {
            if (x+y)%2 == 1 {
                exists = true
                goto yes
            }
        }
    }
yes:
    fmt.Printf("%v\n", exists)
}

It looks like the quantified universal expression is being parsed as a quantified existential expression.

minhnhdo commented 6 years ago

@fhackett, sadly, with the latest rebase to your branch, the bug is still there. There's a reproduction of it as a test case for quantified universals in #83. Could you please take a look at it?

fhackett commented 6 years ago

@mrordinaire that's... interesting. I'll look into that.