From 3a0f90d7b839632344da818ae55fe1c6eea52d7a Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 16 Jul 2013 10:00:19 +0000 Subject: [PATCH] Comments git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7044 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/prism/LTLModelChecker.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/prism/src/prism/LTLModelChecker.java b/prism/src/prism/LTLModelChecker.java index 29cd3835..a9a8bd09 100644 --- a/prism/src/prism/LTLModelChecker.java +++ b/prism/src/prism/LTLModelChecker.java @@ -2,7 +2,7 @@ // // Copyright (c) 2002- // Authors: -// * Carlos S. Bederián (Universidad Nacional de Córdoba) +// * Carlos S. Bederian (Universidad Nacional de Cordoba) // * Dave Parker (University of Oxford, formerly University of Birmingham) // //------------------------------------------------------------------------------ @@ -654,7 +654,7 @@ public class LTLModelChecker * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that * H_i contains Inf(\rho) and the intersection of Inf(K) and L_i is non-empty * - * OTOH PRISM's DRAs (via ltl2dstar use pairs (L_i, K_i) such that + * OTOH PRISM's DRAs (via ltl2dstar) use pairs (L_i, K_i) such that * the intersection of L_i and Inf(\rho) is empty * and the intersection of K_i and Inf(\rho) is non-empty * So: L_i = K_i, H_i = S - L_i @@ -717,7 +717,7 @@ public class LTLModelChecker * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that * H_i contains Inf(\rho) and the intersection of Inf(K) and L_i is non-empty * - * OTOH PRISM's DRAs (via ltl2dstar use pairs (L_i, K_i) such that + * OTOH PRISM's DRAs (via ltl2dstar) use pairs (L_i, K_i) such that * the intersection of L_i and Inf(\rho) is empty * and the intersection of K_i and Inf(\rho) is non-empty * So: L_i = K_i, H_i = S - L_i @@ -805,7 +805,7 @@ public class LTLModelChecker * [dA97] uses Rabin acceptance pairs (H_i, L_i) such that * H_i contains Inf(\rho) and the intersection of Inf(K) and L_i is non-empty * - * OTOH PRISM's DRAs (via ltl2dstar use pairs (L_i, K_i) such that + * OTOH PRISM's DRAs (via ltl2dstar) use pairs (L_i, K_i) such that * the intersection of L_i and Inf(\rho) is empty * and the intersection of K_i and Inf(\rho) is non-empty * So: L_i = K_i, H_i = S - L_i