在合金中减去使用减号功能

Question

我创建了一个自动售货机，它工作正常。一旦交易完成，我想从项目数量中减去1。我在代码中提供了一些意见以供了解。忽略pred巧克力的一些评论。不知何故，我试图减去，但它只是不会。我不知道什么似乎是问题。任何帮助表示赞赏。

sig button { 
     qty:Int} // buttons on vending machine for selecting chocolates 

//sig coin{} 

sig choco{ 
    value:Int, // Each chocolate has some cost as an attribute aka value. 
    choice :one button // Selecting option 
      } 
fact { 
    // all c:choco | all c1:choco -c | c1.choice != c.choice 
     } 
sig machine{ 
    cust : one customer, // Customer entity 
    a,b,c,d,nullb ,ip: one button, // buttons on vending machine ,ip is the input selected by user 
    //oners,twors,fivers ,tenrs,null1: set coin, 
     ipp,opc2 : one Coin, // ipp = input rs , opc = balance rs 
    customeripb: cust one -> one ip, // customer presses a button 
    customeripc: cust one -> one ipp, // customer enters coins 
    customeropc: opc2 one -> one cust, //customer receives balance of coins 
    op: one choco , // output of chocolate from machine 
    customerop: op one -> one cust, // customer receives a chocolate 

    cadbury, kitkat, eclairs , gum,null: lone choco // types of chocolate 
    } 

{ 
    //#(fivers+tenrs+null+twors+oners) = 5 
    #(a+b+c+d) = 4 // no of buttons of a b c and d are 4 on machine 
    # (cadbury+kitkat+ eclairs +gum) =4 // no of options to choose = 4 
    cadbury=choice.a // cadbury corresponds to button a 
    cadbury.value= 10 // cadbury costs 10rs 
     kitkat=choice.b // kitkat corresponds to button b 
     kitkat.value=5 // kitkat costs 5rs 
     null.value=0 // null costs 0 rs 
     null=choice.nullb 
// as such null doesnt exist it is just to specify no i/p no o/p and nulb is an imaginary button 
     eclairs=choice.c // eclairs corresponds to button c 
     eclairs.value=1 // eclairs costs 1 rs 
     gum=choice.d // gum corresponds to button d 
      gum.value=2 // gum costs 1 rs 
      a.qty>=10 and a.qty<=40 
      b.qty>=11 and b.qty<=40 
      c.qty>=12 and c.qty<=40 
      d.qty>=13 and d.qty<=40 

      nullb.qty=0 
    //ip=nullb //input button selection is never nullb(which is imaginary button) 
    ipp.value!=0 // input of coins is never = 0rs 

/* all m:machine|all o:opc2 
    |all opp: op| all i:ip|all ii:ipp| all c:m.cust 
    |c -> i in m.customeripb and c->ii in m.customeripc and o->c in m.customerop and opp->c in m.customerop 
    */ 
    //button=!=none 
} 

sig customer //user of machine 
{ 
} 


abstract sig Coin { //each coin has a valueof rs 
    value: Int 
} 

sig Nullrs extends Coin {} { value = 0 } // void rs 
sig Oners extends Coin {} { value = 1 } // one rs 
sig Twors extends Coin {} { value = 2 } // twors 
sig Fivers extends Coin {}{ value = 5 } // five rs 
sig Tenrs extends Coin {} { value = 10 } // ten rs 

sig Threers extends Coin {} { value = 3 } // this is only used in o/p to specify 3rs will come out 
sig Fourrs extends Coin {} { value = 4 }// this is only used in o/p to specify 4rs will come out 
sig Sixrs extends Coin {} { value = 6 }// this is only used in o/p to specify 6rs will come out 
sig Sevenrs extends Coin {}{ value = 7 }// this is only used in o/p to specify 7rs will come out 
sig Eightrs extends Coin {} { value = 8 } // this is only used in o/p to specify 8rs will come out 
sig Niners extends Coin {} { value = 9} //// this is only used in o/p to specify 9rs will come out 


pred show{} // show 

pred chocolate [before,after:machine ] // machine has two states one before o/p and one after 
    { 

    before.cadbury=after.cadbury 
    before.kitkat=after.kitkat 
    before.eclairs=after.eclairs 
    before.gum=after.gum 

    //all chocolates will not change and are fixed 

    before.ipp.value=after.ipp.value 
// input value of rs remains same i.e i/p is inside machine once inputed so it cant change 
    before.opc2.value=0 // before state o/p value of balance coins =0 
    before.op=before.null // beforestate o/p = no chocolate 
    before.ip!=before.nullb // input button pressed never equals nullb 
    after.ip!=after.nullb // input button pressed never equals nullb 
    //before.ip=after.ip // input button pressed remains same 
    after.op=after.kitkat or after.op=after.eclairs 
     before.null=after.null // imaginary null chocolate remains in same state 

before.opc2!=none and after.opc2 !=none 
// balance of coins is never empty in case of empty I have defined nullrs 


    (after.op.value=before.ipp.value=>after.opc2.value=0) 
    // 
    (after.op=after.null=>after.opc2.value=before.ipp.value) 
    (before.ipp.value > after.op.value=>after.opc2.value=before.ipp.value-after.op.value) 

    //(before.ipp.value=after.op.value=>after.opc2.value=0) 

    //opc2.value!=ipp.value 
    before.ip=before.a or before.ip=before.b or before.ip=before.c or before.ip=before.d 
    (after.op=after.cadbury) => ((after.ip=after.a and after.a.qty=minus[before.a.qty,1])) else 
(after.op=after.kitkat) => ((after.ip=after.b and after.b.qty=minus[before.b.qty, 1])) else 
(after.op=after.eclairs) =>((after.ip=after.c and after.c.qty=minus[before.c.qty,1])) else 
(after.op=after.gum) =>((after.ip=after.d and after.d.qty=minus[before.d.qty,1])) else 
(after.ip=before.ip and after.ip.qty=minus[before.ip.qty,0]) 
after.op!=before.null => after.op.choice=before.ip 
    (after.op=before.gum=>before.ipp.value>=Twors.value) 

    after.op=before.cadbury=>before.ipp.value>=Tenrs.value 
    after.op=before.eclairs=>before.ipp.value>=Oners.value 
    after.op=before.kitkat=>before.ipp.value>=Fivers.value 

(before.ipp=Oners or before.ipp=Twors or before.ipp=Fivers or before.ipp=Tenrs or before.ipp=Nullrs) and 
before.ipp!=Threers and before.ipp!=Fourrs and before.ipp !=Sixrs and before.ipp!=Sevenrs and before.ipp!=Eightrs and before.ipp!=Niners 

(before.ip=before.b and before.ipp.value < 5) => (after.op!=before.kitkat or after.op!=before.eclairs or after.op!=before.cadbury or after.op!=before.gum)and after.op=before.null 
(before.ip=before.d and before.ipp.value < 2) => (after.op!=before.kitkat or after.op!=before.eclairs or after.op!=before.cadbury or after.op!=before.gum)and after.op=before.null 
(before.ip=before.a and before.ipp.value < 10)=> (after.op!=before.kitkat or after.op!=before.eclairs or after.op!=before.cadbury or after.op!=before.gum) and after.op=before.null 
(before.ip=before.c and before.ipp.value >= 1) => (after.op!=before.kitkat or after.op!=before.null or after.op!=before.cadbury or after.op!=before.gum) and after.op=before.eclairs 
(before.ip=before.c and before.ipp.value = 0) => (after.op!=before.kitkat or after.op!=before.null or after.op!=before.cadbury or after.op!=before.gum) and after.op=before.null 
(before.ip=before.a and before.ipp.value =10) => (after.op!=before.kitkat or after.op!=before.null or after.op!=before.eclairs or after.op!=before.gum) and after.op= before.cadbury 
(before.ip=before.d and before.ipp.value >= 2) => (after.op!=before.kitkat or after.op!=before.null or after.op!=before.cadbury or after.op!=before.eclairs) and after.op=before.gum 
(before.ip=before.b and before.ipp.value >= 5) => (after.op!=before.eclairs or after.op!=before.null or after.op!=before.cadbury or after.op!=before.gum) and after.op=before.kitkat 


} 

run chocolate for exactly 2 machine, 8 button, 5 choco,9 Int,5 Coin,1 customer 

Answer 1

一般来说，比“不起作用”更具体一些是有道理的。

我假设你的意思是“它不工作”是你在after机器上所期望的巧克力的数量减少1，而是保持不变。原因是您的(if-then-else) or (if-then-else) or ...表达式，这在逻辑上是有缺陷的。你可能想要表达的是强制执行至少一个分支（因为如果条件满足，你就知道只有一个分支），但是对于满足这个整体分解而言并不是必须的。

更具体而言，在

((after.op=after.cadbury) 
    => (... and after.a.qty=minus[before.a.qty,1] and ...) 
    else (... and after.a.qty=before.a.qty and ...) 
) 
or 
((after.op=after.kitkat) 
    => (... and after.b.qty=minus[before.b.qty,1] and ...) 
    else (... and after.b.qty=before.b.qty and ...) 
) 

即使after.op等于after.cadbury，不执行该条款的然后分支是真实的，因为为满足此整个表达式，它是足以满足下一个条款的其他分支，即所有数量应保持不变。

你需要的是一些软if-then-elsif-...-else结构，例如，

(after.op = after.cadbury) => { 
    ... 
} else (after.op = after.kitkat) => { 
    ... 
} else { 
    ... 
} 

如果你这样做，你的机器还是不行，那就是你的模式将成为不可满足：你的约束可以加强这两个after和before机共享同一个按钮和数量与按钮相关联（所述qty字段是button SIG），这意味着其数量必须在两个after和before机是相同的。我真的没有看到有任何理由把qty放在sig button中。

[1]：通过在你的chocolate谓语before.cadbury=after.cadbury and ...，并且cadbury=choice.a and ...在你的附加事实标志着SIG machine