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 ...は論理的に欠陥のあるあなたの表現です。おそらく表現したかったのは、少なくとも 1 つのthen分岐を強制することです (if 条件が 1 つだけ満たされることがわかっているため) が、この選言全体を満たす必要はありません。

より具体的には、

((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 分岐が true になることは強制されません。これは、この式全体を満たすには、次の句の else 分岐を満たすだけで十分であるため、すべての量が同じままであるべきであるということです。

あなたが望むのは、いくつかのソフトなif-then-elsif-...-else構造です。

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

これを行っても、マシンは機能しません。つまり、モデルが満足できなくなります。制約により、afterとマシンの両方が同じボタン1beforeを共有し、数量がボタンに関連付けられます (フィールドはsig にあります)。つまり、その数量は、とマシンの両方で同じでなければなりません。sigを入れる正当な理由が本当にわかりません。qtybuttonafterbeforeqtybutton

[1]:述語と、before.cadbury=after.cadbury and ...sigの追加の事実に含めることによってchocolatecadbury=choice.a and ...machine

于 2013-04-26T18:44:21.340 に答える