From df436b3734090f1f7b7061ab8f7a8d2deed5cdc6 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 11 May 2007 17:10:40 +0000
Subject: [PATCH] MathML2Prism allows renaming of identifiers.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@331 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/prism/MathML2Prism.java | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/prism/src/prism/MathML2Prism.java b/prism/src/prism/MathML2Prism.java
index 048823c9..b444e5b5 100644
--- a/prism/src/prism/MathML2Prism.java
+++ b/prism/src/prism/MathML2Prism.java
@@ -38,8 +38,11 @@ import org.xml.sax.*;
 public class MathML2Prism
 {
 	// Converts a MathML object to the corresponding PRISM expression (as a string)
+	// (optionally with a list of renames for identifiers)
 	
-	public static String convert(Node node) throws PrismException
+	public static String convert(Node node) throws PrismException { return convert(node, null, null); }
+	
+	public static String convert(Node node, ArrayList renameFrom, ArrayList renameTo) throws PrismException
 	{
 		String s, nodeName, apply;
 		int nodeType, i, n;
@@ -65,7 +68,7 @@ public class MathML2Prism
 				}
 				if (children.size() == 0) throw new PrismException("Empty MathML expression");
 				if (children.size() > 1) throw new PrismException("Too many top-level nodes in MathML expression");
-				return convert(children.get(0));
+				return convert(children.get(0), renameFrom, renameTo);
 			}
 			
 			// Literal
@@ -76,7 +79,11 @@ public class MathML2Prism
 			
 			// Identifier
 			else if (nodeName.equals("ci")) {
+				System.err.println(renameFrom);
+				System.err.println(renameTo);
 				s = node.getFirstChild().getNodeValue().trim();
+				if (renameFrom != null) if (renameFrom.contains(s)) s = (String)renameTo.get(renameFrom.indexOf(s));
+				System.err.println(s);
 				return s;
 			}
 			
@@ -96,7 +103,7 @@ public class MathML2Prism
 				translatedChildren = new ArrayList<String>();
 				n = children.size() - 1;
 				for (i = 0; i < n; i++) {
-					translatedChildren.add(convert(children.get(i+1)));
+					translatedChildren.add(convert(children.get(i+1), renameFrom, renameTo));
 				}
 				
 				// Apply "plus"