。 ＆演算子

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 } 

を書かれている。しかし、私はそれを実行すると、その後、私はこの取得： この/声明<：前身= {代入$ 0->割り当て$ 1、割り当て$ 1->割り当てを$ 1、...}

s.predecessorとt.predecessorは前任関係をとり、最初の要素（それぞれsとt）を投影する必要があります。これはAssignment $ 0.predecessorが{代入$ 1}と代入$ 1.presentecessorも{代入$ 1}を返す必要があります。その後、ユニオン交点（&）を持っていないことは間違いないはずですので、それは事実と矛盾し、現れてはなりません。

私はどこが間違っているか説明できますか？

おかげ

編集：ここでは

は、すべてのコードです。それはかなり長く、他にもいくつかの問題がありますが、問題の部分はそこにあります。私は何が事実に影響を与えることができるか見ることができません。この問題は、実行中の最初の例（私のマシン上）に見られます。

//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の交差点。