了解 .和 & 运算符

Question

我无法理解这些运算符的工作原理。问题如下：我基本上都写了这个

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$1, Assignment$1->Assignment$1, ... }

现在我的理解是，s.predecessor 和 t.predecessor 应该采用前置关系并投影出第一个元素（分别为 s 和 t），这意味着 Assignment$0.predecessor 应该产生 {Assignment$1} 和 Assignment$1。前任也应该产生 {Assignment$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} 

Answer 1

当我在 Alloy 4.2 上运行您的模型时，我没有看到任何错误。也许您可能想在这里分享完整的模型。

关于联合，您需要使用正确的运算符+。 & 用于交叉路口。

基本语法可以参考alloy language reference：

· e1 + e2：e1 和 e2 的并集；
· e1 - e2：e1和e2的区别；
· e1 & e2：e1和e2的交集；