Понимание . и & оператор

Мне трудно понять, как работают эти операторы. Проблема в следующем: я в основном написал это

abstract sig Statement {
    predecessor: lone Statement
    --...
}
sig Assignment extends Statement{
    --...
}
--Statements have unique prdecessors
fact { all disj s, t: Statement | s.predecessor & t.predecessor = none }

Но затем, когда я запускаю его, я получаю следующее: this/Statement‹:predecessor={Assignment$0->Assignment$1, Assignment$1->Assignment$1, ... }

Как я понимаю, s.predecessor и t.predecessor должны брать отношение предшественника и проецировать первый элемент (s и t соответственно), что означает, что Assignment$0.predecessor должен давать {Assignment$1}, а Assignment$1.predecessor должен давать {Назначение $1} также. Тогда взятие пересечения union (&) из них определенно не должно быть none, поэтому оно противоречит факту и не должно появляться.

Не могли бы вы объяснить, где я ошибся?

Спасибо

Редактировать:

Вот и весь код. Он довольно длинный, и есть некоторые другие проблемы, но рассматриваемые части там есть. Я не вижу, как что-то может повлиять на этот факт. Проблема видна в первом примере при его запуске (во всяком случае, на моей машине).

//Signatures

//specification

--Expressions
abstract sig Expr{
    type: one Type,
    subExprs: set Expr
}

--Literals
sig Literal extends Expr{}
{ no subExprs }

--Variables
sig Variable{
    type: Type
}

--Functions
sig Function{
    statements: set Statement,
    returnType: one Type,
    params: set FormalParameter
}

--Statements
abstract sig Statement {
    exprs: set Expr,
    predecessor: lone Statement
}

--Variable Declarations
sig VarDecl extends Statement{
    var: Variable
}
{ no exprs }

--Types
sig Type{
    super: lone Type
}

--Formal Parameters
sig FormalParameter{
    type: Type,
    var: Variable
}

//more

--Call Expressions
sig CallExpr extends Expr{
    funct: Function,
    mapping: subExprs -> FormalParameter
}
//not modeled: order of parameters is the same as order of exprs

--Varaible References
sig Reference extends Expr{
    var: Variable
}
{ no subExprs }

--Return Statement
sig Return extends Statement{}
{ one exprs }

--Variable Assignment
sig Assignment extends Statement{
    var: Variable
}
{ one exprs }

--Main Function
one sig Main extends Function{}  




//==========================================================================
//Functions

//specification

--number of function calls in the program
fun p_numFunctionsCalls[]: Int{
    #CallExpr
}

--returns the types of all expressions
fun p_literalTypes[]: set Type{
    Expr.type // not sure if multiples allowed
}

--Returns all statements directly contained in the body of a function
fun p_statementsInFunction[f: Function]: set Statement{
    f.statements
}

--Returns all statements contained after s in the same function
fun p_statementsAfter[s: Statement]: set Statement{
    { fs: Statement | s in fs.^predecessor } 
}

--Returns the formal parameters of function f
fun p_parameters[f: Function]: FormalParameter{
    {ps: f.params}
}

--Returns the direct subexpressions of e
fun p_subExprs[e: Expr]: set Expr{
    e.subExprs
}

//more

--Returns all Expression in a function
fun p_funExprs[f: Function]: set Expr{
     p_statementExprs[f.statements]
}

--Returns all callExpressions in a function
fun p_funCallExprs[f: Function]: set CallExpr{
    { ce: CallExpr | ce in  p_funExprs[f]}
}

--Returns all exprs in s
fun p_statementExprs[s: Statement]: set Expr{
    s.exprs.*subExprs
}

--Returns all references in statements
fun p_statementReferences[s: Statement]: set Reference{
    { r: Reference | r in s.p_statementExprs }
}

--Returns all variable Declarations in f
fun p_funVarDecls[f: Function]: set VarDecl{
    { vd: VarDecl | vd in f.statements }
}

--Returns all variables declared in f
fun p_funVars[f: Function]: set Variable{
    { v: Variable | v in f.p_funVarDecls.var }
}

--return all subTypes of t and t itself
fun p_subTypes[t: Type]: set Type{
    { st: Type | t in st.*super }
}


//==========================================================================
//Predicates

//specification

--true iff f contains a function call directly in its body
pred p_containsCall[f: Function]{
    { some ce: CallExpr | ce in f.statements.exprs.*subExprs }
}

--true iff v appears on the left side of an assignment anywhere the program
pred p_isAssigned[v: Variable]{
    v in Assignment.var
}

--true iff v appears in an expression anywhere the program
pred p_isRead[v: Variable]{
    v in Reference.var
}

--true iff v is declared exactly once
pred p_isDeclared[v: Variable]{
    { all disj a, b: VarDecl | v = a.var implies v != b.var }
}

--true iff v is declared as a parameter
pred p_isParameter[v: Variable]{
    { all vd: VarDecl | v not in vd.var }//FIXME: variable might not be declared at all
}

--true iff t1 is a subtype of t2
pred p_subtypeOf[t1: Type, t2: Type]{
    t1 in t2.super
}

--true iff s assigns to the variable declared by vd
pred p_assignsTo[s: Statement, vd: VarDecl]{
    { all a: Assignment | s in a implies vd.var = a.var }
}

//more

//==========================================================================
//Facts

--All statements are in functions
fact { all s: Statement | s in Function.statements }

--Statements unique to functions
fact { all s: Statement, disj f, g: Function |  s in f.statements implies s not in g.statements }

--Statement predecessors are in same function
fact { all s: Statement, f: Function | s in f.statements implies s.p_statementsAfter in f.statements }

--Statements have unique prdecessors
fact { all disj s, t: Statement | s.predecessor & t.predecessor = none }


--return is always last
fact { all r: Return, f: Function | r in f.statements implies r.^predecessor = f.statements - r} 

--return has the same type as function its in
fact { all r: Return, f: Function | r in f.statements implies r.exprs.type in f.returnType.p_subTypes }



--assignments are only used after vars are declared
fact { all a: Assignment, vd: VarDecl | a.var in vd.var implies a in vd.p_statementsAfter }

--assignment and variable type match
fact { all a: Assignment | a.subExprs.type = a.var.type.p_subTypes }


--references only reference variables of the same function
fact { all r: Reference, f: Function | r in f.p_funExprs implies (r.var in f.params.var  or  r.var in f.p_funVars) }

--references only reference declared variables, all variables are referenced
fact { all f: Function | p_statementReferences[f.statements].var = f.p_funVars }

--type of the reference is type of the variable
fact { all r: Reference | r.type in r.var.type.p_subTypes }



--all functions have a return
fact { all f: Function | Return & f.statements != none }

--all functions but main are called
fact { all f: Function | f not in Main implies f in CallExpr.funct }

--recursion is not allowed
fact { all f: Function | f not in f.p_funCallExprs.*funct }


--each expression only in one statement
fact { all disj s, t: Statement | s.p_statementExprs & t.p_statementExprs = none }

--all expressions in statements
fact { all e: Expr | e in p_statementExprs[Statement] }

--expression not in its subExprs
fact { all e: Expr | e not in e.^subExprs }

--subExpressions unique
fact { all disj c, d, e: Expr | c in d.subExprs implies c not in e.subExprs }


--main never called
fact { Main not in CallExpr.funct }

--main has no params
fact { Main.params = none }


--types not supertytes of themselves
fact { all t: Type | t not in t.^super }


--variables always declared in either callExprs or varDecls
fact { all v: Variable | (v in VarDecl.var iff v not in FormalParameter.var) and (v in FormalParameter.var iff v not in VarDecl.var) }

--variables only declared once in varDecls
fact { all disj u, v: VarDecl | u.var != v.var }

--variables only declared once as parameters / parameters map to unique variable
fact { all disj fp1, fp2: FormalParameter | fp1.var != fp2.var }

--variables have the same type as corresponding param
fact { all fp: FormalParameter | fp.type = fp.var.type }

--declared variables are used always after the declaration and never before
fact { all vd: VarDecl | vd.var in vd.p_statementsAfter.p_statementReferences.var and  vd.var not in vd.^predecessor.p_statementReferences.var }


--parameters are never assigned to
fact { all fp: FormalParameter | fp.var not in Assignment.var }

--all parameters are in functions
fact { all fp: FormalParameter | fp in Function.params }

--params are unique to functions
fact { all fp: FormalParameter, disj f, g: Function | fp in f.params implies fp not in g.params }


--only params of function are mapped to
fact { all ce: CallExpr, expr: ce.subExprs | ce.mapping[expr] in ce.funct.params }

--callExprs have correct type
fact { all ce: CallExpr | ce.type = ce.funct.returnType }

--types of mapping are correct
fact { all ce: CallExpr, expr: ce.subExprs, p: ce.funct.params | ce.mapping[expr] = p implies expr.type = p.type }

--callExpr mapping is unique
fact { all ce: CallExpr, disj expr1, expr2: ce.subExprs | ce.mapping[expr1] != ce.mapping[expr2] }

--all subExprs are being mapped
fact { all ce: CallExpr | #ce.subExprs = #ce.funct.params } 


/*
--references have the same type as their variable
fact { all r: Reference | r.type = r.var.type }


*/


//==========================================================================
//Assertions



//==========================================================================
//Run

pred show{ all ce: CallExpr | #ce.subExprs >= 2}
pred show2{#Literal >= 3}
run {show2}