From 684d2bf93e5bc6e321ba4b08902e236a8b400eee Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 27 Mar 2020 07:59:35 +0000
Subject: [PATCH] Parse fraction test RESULT specs with BigRational even in
 non-exact mode.

---
 .../normaltestwithrationalresult.prism        | 131 ++++++++++++++++++
 .../normaltestwithrationalresult.prism.props  |   2 +
 prism/src/parser/ast/Property.java            |   4 +-
 3 files changed, 134 insertions(+), 3 deletions(-)
 create mode 100644 prism-tests/bugfixes/normaltestwithrationalresult.prism
 create mode 100644 prism-tests/bugfixes/normaltestwithrationalresult.prism.props

diff --git a/prism-tests/bugfixes/normaltestwithrationalresult.prism b/prism-tests/bugfixes/normaltestwithrationalresult.prism
new file mode 100644
index 00000000..73dd198d
--- /dev/null
+++ b/prism-tests/bugfixes/normaltestwithrationalresult.prism
@@ -0,0 +1,131 @@
+// bounded retransmission protocol [D'AJJL01]
+// gxn/dxp 23/05/2001
+
+dtmc
+
+// number of chunks
+const int N = 16;
+// maximum number of retransmissions
+const int MAX = 2;
+
+module sender
+
+	s : [0..6];
+	// 0 idle
+	// 1 next_frame	
+	// 2 wait_ack
+	// 3 retransmit
+	// 4 success
+	// 5 error
+	// 6 wait sync
+	srep : [0..3];
+	// 0 bottom
+	// 1 not ok (nok)
+	// 2 do not know (dk)
+	// 3 ok (ok)
+	nrtr : [0..MAX];
+	i : [0..N];
+	bs : bool;
+	s_ab : bool;
+	fs : bool;
+	ls : bool;
+	
+	// idle
+	[NewFile] (s=0) -> (s'=1) & (i'=1) & (srep'=0);
+	// next_frame
+	[aF] (s=1) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=0);
+	// wait_ack
+	[aB] (s=2) -> (s'=4) & (s_ab'=!s_ab);
+	[TO_Msg] (s=2) -> (s'=3);
+	[TO_Ack] (s=2) -> (s'=3);
+	// retransmit
+	[aF] (s=3) & (nrtr<MAX) -> (s'=2) & (fs'=(i=1)) & (ls'=(i=N)) & (bs'=s_ab) & (nrtr'=nrtr+1);
+	[] (s=3) & (nrtr=MAX) & (i<N) -> (s'=5) & (srep'=1);
+	[] (s=3) & (nrtr=MAX) & (i=N) -> (s'=5) & (srep'=2);
+	// success
+	[] (s=4) & (i<N) -> (s'=1) & (i'=i+1);
+	[] (s=4) & (i=N) -> (s'=0) & (srep'=3);
+	// error
+	[SyncWait] (s=5) -> (s'=6); 
+	// wait sync
+	[SyncWait] (s=6) -> (s'=0) & (s_ab'=false); 
+	
+endmodule
+
+module receiver
+
+	r : [0..5];
+	// 0 new_file
+	// 1 fst_safe
+	// 2 frame_received
+	// 3 frame_reported
+	// 4 idle
+	// 5 resync
+	rrep : [0..4];
+	// 0 bottom
+	// 1 fst
+	// 2 inc
+	// 3 ok
+	// 4 nok
+	fr : bool;
+	lr : bool;
+	br : bool;
+	r_ab : bool;
+	recv : bool;
+	
+	
+	// new_file
+	[SyncWait] (r=0) -> (r'=0);
+	[aG] (r=0) -> (r'=1) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+	// fst_safe_frame
+	[] (r=1) -> (r'=2) & (r_ab'=br);
+	// frame_received
+	[] (r=2) & (r_ab=br) & (fr=true) & (lr=false)  -> (r'=3) & (rrep'=1);
+	[] (r=2) & (r_ab=br) & (fr=false) & (lr=false) -> (r'=3) & (rrep'=2);
+	[] (r=2) & (r_ab=br) & (fr=false) & (lr=true)  -> (r'=3) & (rrep'=3);
+	[aA] (r=2) & !(r_ab=br) -> (r'=4);  
+	// frame_reported
+	[aA] (r=3) -> (r'=4) & (r_ab'=!r_ab);
+	// idle
+	[aG] (r=4) -> (r'=2) & (fr'=fs) & (lr'=ls) & (br'=bs) & (recv'=T);
+	[SyncWait] (r=4) & (ls=true) -> (r'=5);
+	[SyncWait] (r=4) & (ls=false) -> (r'=5) & (rrep'=4);
+	// resync
+	[SyncWait] (r=5) -> (r'=0) & (rrep'=0);
+	
+endmodule
+	
+module checker
+
+	T : bool;
+	
+//	[NewFile] (T=false) -> (T'=false);
+	[NewFile] (T=false) -> (T'=true);
+	
+endmodule
+
+module	channelK
+
+	k : [0..2];
+	
+	// idle
+	[aF] (k=0) -> 0.98 : (k'=1) + 0.02 : (k'=2);
+	// sending
+	[aG] (k=1) -> (k'=0);
+	// lost
+	[TO_Msg] (k=2) -> (k'=0);
+	
+endmodule
+
+module	channelL
+
+	l : [0..2];
+	
+	// idle
+	[aA] (l=0) -> 0.99 : (l'=1) + 0.01 : (l'=2);
+	// sending
+	[aB] (l=1) -> (l'=0);
+	// lost
+	[TO_Ack] (l=2) -> (l'=0);
+	
+endmodule
diff --git a/prism-tests/bugfixes/normaltestwithrationalresult.prism.props b/prism-tests/bugfixes/normaltestwithrationalresult.prism.props
new file mode 100644
index 00000000..0dd68fbb
--- /dev/null
+++ b/prism-tests/bugfixes/normaltestwithrationalresult.prism.props
@@ -0,0 +1,2 @@
+// RESULT: 1503982516387544510687823213516750681753609533738014093985492327446021823341670745201522478360759626261166470522913554557570937367804047825330483938531949304640395637223627199/3552713678800500929355621337890625000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
+"p1": P=? [ F s=5 ];
diff --git a/prism/src/parser/ast/Property.java b/prism/src/parser/ast/Property.java
index 477c6a8c..8e5e5a7b 100644
--- a/prism/src/parser/ast/Property.java
+++ b/prism/src/parser/ast/Property.java
@@ -398,9 +398,7 @@ public class Property extends ASTElement
 				}
 				// See if it's a fraction
 				else if (strExpectedValue.matches("[0-9]+/[0-9]+")) {
-					int numer = Integer.parseInt(strExpectedValue.substring(0, strExpectedValue.indexOf('/')));
-					int denom = Integer.parseInt(strExpectedValue.substring(strExpectedValue.indexOf('/') + 1));
-					doubleExp = ((double) numer) / denom;
+					doubleExp = new BigRational(strExpectedValue).doubleValue();
 					simple = false;  // complex expression
 				}
 				// Otherwise, see if it's just a double