0

我创建了一台自动售货机，它工作正常。交易完成后，我想从商品数量中减去 1。我在代码中提供了注释以供理解。忽略pred Chocolate中的一些评论。不知何故，我试图减去，但它不会。我不知道似乎是什么问题。任何帮助表示赞赏。 

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
4

1 回答 1

1

一般来说，比“它不起作用”更具体是有意义的。

我假设您所说的“它不起作用”的意思是在after机器中您希望所选巧克力的数量减少 1，但相反，它保持不变。原因是你的(if-then-else) or (if-then-else) or ...表达方式，逻辑上有缺陷。您可能想要表达的是强制执行至少一个then分支（因为您知道恰好满足一个 if 条件），但这对于满足整个析取而言并不是必需的。

更具体地说，在

((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，也不会强制该子句的 then 分支为真，因为要满足整个表达式，足以满足下一个子句的 else 分支，即所有数量都应保持不变。

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

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

如果您这样做，您的机器仍然无法工作，也就是说，您的模型将变得无法满足：您的约束强制要求after和before机器共享相同的按钮1并且数量与按钮相关联（该qty字段在buttonsig 中），这意味着after和before机器中的数量必须相同。我真的看不出有什么好的理由去qtysig button。

[1]：通过before.cadbury=after.cadbury and ...在你的chocolate谓词和cadbury=choice.a and ...附加的事实中加入 sigmachine

于 2013-04-26T18:44:21.340 回答