From 3ff9514f7bfbc895b9995413d483568760ba673b Mon Sep 17 00:00:00 2001 From: gereon Date: Wed, 1 May 2013 02:00:10 +0200 Subject: [PATCH] Make clone() work for variables without initial value. --- examples/dtmc/synchronous_leader/leader3_5.pm | 24 +++++++++---------- src/ir/Variable.cpp | 8 +++++-- 2 files changed, 18 insertions(+), 14 deletions(-) diff --git a/examples/dtmc/synchronous_leader/leader3_5.pm b/examples/dtmc/synchronous_leader/leader3_5.pm index 2a5e200dc..0703e733d 100644 --- a/examples/dtmc/synchronous_leader/leader3_5.pm +++ b/examples/dtmc/synchronous_leader/leader3_5.pm @@ -15,15 +15,15 @@ module counter c : [1..N-1]; // reading - [read] c (c'=c+1); + [read] c 1:(c'=c+1); // finished reading - [read] c=N-1 -> (c'=c); + [read] c=N-1 -> 1:(c'=c); //decide - [done] u1|u2|u3 -> (c'=c); + [done] u1|u2|u3 -> 1:(c'=c); // pick again reset counter - [retry] !(u1|u2|u3) -> (c'=1); + [retry] !(u1|u2|u3) -> 1:(c'=1); // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (c'=c); + [loop] s1=3 -> 1:(c'=c); endmodule @@ -56,18 +56,18 @@ module process1 + 1/K : (s1'=1) & (p1'=3) & (v1'=3) & (u1'=true) + 1/K : (s1'=1) & (p1'=4) & (v1'=4) & (u1'=true); // read - [read] s1=1 & u1 & c (u1'=(p1!=v2)) & (v1'=v2); - [read] s1=1 & !u1 & c (u1'=false) & (v1'=v2) & (p1'=0); + [read] s1=1 & u1 & c 1:(u1'=(p1!=v2)) & (v1'=v2); + [read] s1=1 & !u1 & c 1:(u1'=false) & (v1'=v2) & (p1'=0); // read and move to decide - [read] s1=1 & u1 & c=N-1 -> (s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); - [read] s1=1 & !u1 & c=N-1 -> (s1'=2) & (u1'=false) & (v1'=0); + [read] s1=1 & u1 & c=N-1 -> 1:(s1'=2) & (u1'=(p1!=v2)) & (v1'=0) & (p1'=0); + [read] s1=1 & !u1 & c=N-1 -> 1:(s1'=2) & (u1'=false) & (v1'=0); // deciding // done - [done] s1=2 -> (s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); + [done] s1=2 -> 1:(s1'=3) & (u1'=false) & (v1'=0) & (p1'=0); //retry - [retry] s1=2 -> (s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); + [retry] s1=2 -> 1:(s1'=0) & (u1'=false) & (v1'=0) & (p1'=0); // loop (when finished to avoid deadlocks) - [loop] s1=3 -> (s1'=3); + [loop] s1=3 -> 1:(s1'=3); endmodule diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp index 4edc93b2f..082011655 100644 --- a/src/ir/Variable.cpp +++ b/src/ir/Variable.cpp @@ -25,8 +25,12 @@ Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_pt // Nothing to do here. } -Variable::Variable(const Variable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints) - : Variable(var.index, newName, var.initialValue->clone(renaming, bools, ints)) { +Variable::Variable(const Variable& var, const std::string& newName, const std::map& renaming, const std::map& bools, const std::map& ints) { + this->index = var.index; + this->variableName = newName; + if (var.initialValue != nullptr) { + this->initialValue = var.initialValue->clone(renaming, bools, ints); + } } // Return the name of the variable.