From 70cd7742ee74295ea07124fdd169d194038f1ded Mon Sep 17 00:00:00 2001
From: Philip Offtermatt <p.offtermatt@gmail.com>
Date: Mon, 16 Oct 2023 10:40:47 +0200
Subject: [PATCH] Use ... syntax

---
 tests/difference/core/quint_model/ccv.qnt | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

diff --git a/tests/difference/core/quint_model/ccv.qnt b/tests/difference/core/quint_model/ccv.qnt
index 5ea3d8f4a7..8cab951c99 100644
--- a/tests/difference/core/quint_model/ccv.qnt
+++ b/tests/difference/core/quint_model/ccv.qnt
@@ -620,30 +620,25 @@ module ccv {
                 List()
             }
         )
-        providerState.with(
-            // send VscPackets to consumers
-            "outstandingPacketsToConsumer",
-            ConsumerChains.mapBy(
+        val newOutstandingPacketsToConsumer = ConsumerChains.mapBy(
                 (consumer) => 
                 providerState.outstandingPacketsToConsumer.get(consumer).concat(
                     newSentPacketsPerConsumer.get(consumer)
                 )
             )
-            ).with(
-                // update the sent VscPackets
-                "sentVscPacketsToConsumer",
-                ConsumerChains.mapBy(
+        val newSentVscPackets = ConsumerChains.mapBy(
                     (consumer) => 
                     providerState.sentVscPacketsToConsumer.get(consumer).concat(
                         newSentPacketsPerConsumer.get(consumer)
                     )
                 )
-            ).with(
-                // the validator set has not changed yet in the new block
-                "providerValidatorSetChangedInThisBlock", false
-            ).with(
-                "runningVscId", providerState.runningVscId + 1
-            )
+        {
+            ...providerState,
+            outstandingPacketsToConsumer: newOutstandingPacketsToConsumer,
+            sentVscPacketsToConsumer: newSentVscPackets,
+            providerValidatorSetChangedInThisBlock: false,
+            runningVscId: providerState.runningVscId + 1,
+        }
     }
 
     // receives a given packet (sent by the provider) on the consumer. The arguments are the consumer chain that is receiving the packet, and the packet itself.