Generating list of fixed value in alloy

Question

I am trying to create a list of coins which denote a value.suppose 9 rs will contain a sequence 5->2->2 . 8rs will have 5rs->2rs->1rs. 7rs will have 5->2 . The coins can be of the type 10Rs, 5rs, 2rs,1rs. Here in this code tenr implies list of coins of value ten and tenrs implies coin of ten rs. How can I create such a list? I've been trying but all in vain . Also when I execute and click on show it shows multiple coins assigned to a single coin node. Any help will be appreciated. Actually I am trying to use it in a vending machine. I checked your code and I am currently trying to implement it . I am also providing my code for vending machine.

sig coin{}

sig oners,twors,fivers,tenrs,null1 in coin {}

sig list
{

next :  coin lone -> lone coin
}


sig oner,twor,threer,fourr,sixr,sevenr,eightr,niner,fiver,tenr,nullr in list {}

fact {
    //  all c:choco | all c1:choco -c | c1.choice != c.choice
    //  all m: machine| some n:m.null1 | some ors: m.oners| ors->n in (m.oner).next
    all  l:list| all c:coin| c->c not  in l.next
    all  l:list|no c : coin | (c in c.^(l.next ))
    //all m: machine| all o:m.oner | oners->null1 in o
   all o:oner| all n: null1|all l:list|oners->null1 in o.next and #n.(l.next)=0
            all n:nullr| all n1:null1| #n1.(n.next)= 1  and #(n.next).n1=0 and n1->null1 in n.next
    all t:tenr| all tr:tenrs | #tr.(t.next)= 1 and #(t.next).tr=0 and tr->null1 in t.next
all t:twor| all tr:twors | #tr.(t.next)= 1 and #(t.next).tr=0 and tr->null1 in t.next
}

---

Vending machine

sig button {}

sig coin{}

sig choco{
    value:one coin,
    choice :one button
            }
fact {
        all c:choco | all c1:choco -c | c1.choice != c.choice
        }
sig machine{
    a,b,c,d : one button,
    oners,twors,fivers ,tenrs,null1: set coin,
    cadbury, kitkat, eclairs , gum,null: lone choco
    }

{
  #(fivers+tenrs+null+twors+oners) = 5 
  #(a+b+c+d) = 4
    #   (cadbury+kitkat+ eclairs +gum) =4
    cadbury=choice.a
    cadbury= value.tenrs
        kitkat=choice.b
        kitkat=value.fivers
        eclairs=choice.c
        eclairs=value.oners
        gum=choice.d
            gum=value.twors
}

pred show{}

pred chocolate [before,after:machine , x: coin, op:choco, opc: coin, ip:button]
    {
    before.a=after.a
    before.b=after.b
    before.c=after.c
    before.d=after.d
    before.cadbury=after.cadbury
    before.kitkat=after.kitkat
    before.eclairs=after.eclairs
    before.gum=after.gum
    before.null1=after.null1
    before.oners=after.oners
    before.twors=after.twors
    before.fivers=after.fivers
    before.tenrs=after.tenrs
        before.null=after.null
    x = before.oners or x= before.twors or x= before.fivers or x= before.tenrs
    ip = before.a or ip = before.b or ip=before.c or ip = before.d 
    ip=before.a =>op=before.cadbury or op=none

        ip=before.b =>op=before.kitkat or op=none

    ip=before.c =>op=before.eclairs or op=none

    ip=before.d =>op=before.gum or op=none
    op=before.gum=>x=before.twors
    op=before.cadbury=>x=before.tenrs
    op=before.eclairs=>x=before.oners
    op=before.kitkat=>x=before.fivers
    (ip=before.c and x=before.oners =>op=after.eclairs and opc=after.null1)
    or   
    (ip=before.c and x=before.twors =>op=after.eclairs and opc=after.oners)
    or
        (ip=before.c and x=before.fivers =>op=after.eclairs and opc=after.twors)
    or
        (ip=before.c and x=before.tenrs =>op=after.eclairs and opc=after.fivers)
    or
    (ip=before.c and x=before.null1 =>op=after.null and opc=after.null1)
or
(ip=before.d and x=before.twors =>op=after.gum and opc=after.null1)
    or
(ip=before.d and x=before.oners =>op=after.null and opc=after.oners)
or
(ip=before.d and x=before.fivers =>op=after.gum and opc=after.twors)
or
(ip=before.d and x=before.tenrs =>op=after.gum and opc=after.fivers)
or
    (ip=before.d and x=before.null1 =>op=after.null and opc=after.null1)
or
(ip=before.b and x=before.fivers =>op=after.kitkat and opc=after.null1)   
    or
(ip=before.b and x=before.tenrs =>op=after.kitkat and opc=after.fivers)
or 
(ip=before.b and x=before.oners =>op=after.null and opc=after.oners)
or
(ip=before.b and x=before.twors =>op=after.null and opc=after.twors)
or
    (ip=before.b and x=before.null1 =>op=after.null and opc=after.null1)
or
    (ip=before.a and x=before.tenrs =>op=after.cadbury and opc=after.null1)
or
    (ip=before.a and x=before.fivers =>op=after.null and opc=after.fivers)
or
    (ip=before.a and x=before.twors =>op=after.null and opc=after.twors)
or
    (ip=before.a and x=before.null1 =>op=after.null and opc=after.null1)
}

run chocolate for exactly 2 machine, 8 button, 8 choco, 10 coin

Answer 1

abstract sig Coin {
  value: Int
}

sig Oners extends Coin {} { value = 1 }
sig Twors extends Coin {} { value = 2 }
sig Fivers extends Coin {}{ value = 5 }
sig Tenrs extends Coin {} { value = 10 }

sig List {
  coins: seq Coin
}

pred sumTo(l: List, val: Int) {
  (sum idx: l.coins.Coin | l.coins[idx].value) = val
}

run {
  //some l5: List | sumTo[l5, 5]
  some l10: List | sumTo[l10, 10]
} for 10 but 5 Int