합금에서 빼기 함수를 사용하여 빼기

Question

자동 판매기를 만들었으므로 잘 작동합니다. 트랜잭션이 완료되면 항목 수에서 1을 뺍니다. 이해를 돕기 위해 내 코드에 주석을 제공했습니다. 프리디 초콜렛의 일부 댓글을 무시하십시오. 어쨌든 나는 빼는 것을 시도하고있다 그러나 그것은 다만 실 거예요. 나는 그 문제가 무엇인지 모릅니다. 어떤 도움을 주셔서 감사합니다.

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 ... 표현입니다. 당신이 표현하기를 원하는 것은 최소한 하나의 then 브랜치를 적용하는 것입니다 (조건이 충족 될 경우 정확히 하나를 알고 있기 때문에).하지만이 모든 분리를 만족시킬 필요는 없습니다. 이 모든 표현을 만족시키기 때문에, 사실 해당 조항의 다음 분기를 적용하지 않습니다 after.op가 after.cadbury 동일한 경우에도

((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 ...) 
) 

에서보다 구체적으로

은,을 만족하기에 충분 else 절은 모든 항이 동일하게 유지되어야한다고 말합니다. 당신이 원하는 것은 예를 들어, if-then-elsif-...-else 구조의 일부 부드럽고

,

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

당신이 당신의 기계가 여전히 작동하지 않는 것을하는 경우, 즉, 모델이 시켰음이 될 것이다 : 당신의 제약 조건을 모두 after를 적용하는 before 컴퓨터는 동일한 버튼 을 공유하며 수량은 버튼과 관련이 있습니다 (qty 필드는 button 시그)이므로 after과 before 기계에서 수량이 동일해야합니다. sig button에 qty을 넣을만한 이유가 없습니다.

[1] : 또한 작동하지 않습니다 시작시에 열린 폴더의 유틸리티/정수를 추가 machine