the scripting for experiments wermer2 should now be ready

experiments/tools/t3daikon/build.xml

+<project default="compile">
+    
+<target name="compile">
+    <javac includeantruntime="true" 
+               srcdir="./src"
+               classpath="T3.jar;T3daikon.jar"
+               destdir="."
+               debug="yes">
+    </javac>
+</target> 
+    
+</project>

experiments/tools/t3daikon/src/MyDaikonUtils.java

+
+
+import Sequenic.T3.Daikon.*;
+import Sequenic.T3.Sequence.Datatype.SUITE;
+
+/**
+ * Provide top-level functions to infer and check Daikon invariants from/on a T3 test suite.
+ */
+public class MyDaikonUtils {
+	
+	/**
+	 * Use a T3 test suite to drive executions on the suite's target class, and then infer 
+	 * Daikon-invariants from these executions. The inferred invariants will be saved on the 
+	 * specified file name (should end with .inv).
+	 * 
+	 * This will also generate a trace file containing collected run-time values of the parameters
+	 * passed to methods when they are called during the executions, and the values they return.
+	 * The trace file has .dtrace extension.
+	 */
+	static void mineInvariants(SUITE S, String targetMethod, String invariantsFile) throws Exception {
+		String prefix = invariantsFile ;
+		if (invariantsFile.endsWith(".inv")) prefix = invariantsFile.substring(0, invariantsFile.length() - 4) ;
+		(new T3Daikon()).infer(S, targetMethod, prefix + ".dtrace", prefix + ".inv");
+	}
+	
+    void mineInvariants(String saved_T3_testsuite_file, String targetMethod, String invariantsFile) throws Exception {
+		SUITE S = SUITE.load(saved_T3_testsuite_file) ;
+		mineInvariants(S,targetMethod,invariantsFile) ;
+	}
+	
+	/**
+	 * Read invariants from the specified file; then check the invariants on the executions generated 
+	 * by the given T3 test suite. If no violation is found, true is returned, else false. This 
+	 * is also echoed to System.out.
+	 * 
+	 * If there are violations, a _violations.txt file is generated that contains further details
+	 * on the violations.
+	 */
+	static boolean checkInvariants(SUITE S, String targetMethod, String invariantsFile) throws Exception{
+		String prefix = invariantsFile ;
+		if (invariantsFile.endsWith(".inv")) prefix = invariantsFile.substring(0, invariantsFile.length() - 4) ;
+		invariantsFile = prefix + ".inv" ;
+		String violationsReportFile = prefix + "_violations.txt" ;
+		return (new T3Daikon()).check(S,targetMethod,invariantsFile,violationsReportFile) ;
+	}
+	
+	static boolean checkInvariants(String saved_T3_testsuite_file, String targetMethod, String invariantsFile) throws Exception{
+		SUITE S = SUITE.load(saved_T3_testsuite_file) ;
+		return checkInvariants(S,targetMethod,invariantsFile) ;
+		
+	}
+
+}

experiments/wermer2/t3daikongen/MyT3SuiteGenerator.java → experiments/tools/t3daikon/src/MyT3.java

@@ -19,7 +19,10 @@ import Sequenic.T3.Info.JacocoInstrumenter;
 import Sequenic.T3.Sequence.Datatype.*;
 import static Sequenic.T3.Generator.Value.ValueMGCombinators.* ;
 
-public class MyT3SuiteGenerator {
+/**
+ * Provide a wrapper class around T3 to make it easier to deply for the experiments.
+ */
+public class MyT3 {
 
 	/**
 	 * T3, which is the actual worker of this generator.
@@ -49,7 +52,7 @@ public class MyT3SuiteGenerator {
 	 * Class Under Test (CUT). In addition, you can pass on a custom primitive-values generator. 
 	 * Use null if you do not want to pass a custom generator.
 	 */
-	public MyT3SuiteGenerator(Config configTemplate, 
+	public MyT3(Config configTemplate, 
 			         String CUTrootDir, 
 			         String classname, 
 			         Sequenic.T3.Generator.Generator<PARAM,STEP> custom_values_generator) 
@@ -186,9 +189,9 @@ public class MyT3SuiteGenerator {
 	
 	
 	/**
-	 * The function to generate T3 suite for a given target.
+	 * A top level function to generate T3 suite for a given target. 
 	 */
-	static public void generate(
+	static public SUITE generate(
 			Sequenic.T3.Generator.Generator<PARAM,STEP> my_custom_values_generator, 
 			String CUTrootDir,
 			String CUT, 
@@ -198,44 +201,12 @@ public class MyT3SuiteGenerator {
 			String saveFile,
 			String reportFile) throws Exception 
 	{
-		MyT3SuiteGenerator gen = new MyT3SuiteGenerator(mkStandardTemplateOfT3Configuration(),CUTrootDir,CUT,my_custom_values_generator) ;
-		gen.generate_(targetMethod,desiredSuiteSize,maximumNumberOfTestSequences_to_try,saveFile,reportFile) ;	
+		MyT3 gen = new MyT3(mkStandardTemplateOfT3Configuration(),CUTrootDir,CUT,my_custom_values_generator) ;
+		SUITE S = gen.generate_(targetMethod,desiredSuiteSize,maximumNumberOfTestSequences_to_try,saveFile,reportFile) ;
+		return S ;
 	}
 	
 	
-	static String ExperimentHome = "/Users/iswbprasetya/workshop/projects/koenwlp/repo/javawlp/experiments/wermer2" ;
-	static String XCUTrootdir = ExperimentHome + "/subjects/compiled" ;
-	static String XDatadir = ExperimentHome + "/data" ;
-	static String XT3suitedir = ExperimentHome + "/tests/t3suite" ;
-	static int XdesiredSuiteSize = 1000 ;
-	static int XmaximumNumberOfTestSequences_to_try = 5000 ;
-	
-	static void genSuiteTriangle() throws Exception {
-		Sequenic.T3.Generator.Generator<PARAM,STEP> customgen = Float(OneOf(-1f,0f,1f,1.1f,2f,3f,9f)) ;
-		String CUT = "Triangle" ;
-		generate(customgen,XCUTrootdir,CUT,"tritype1",
-				XdesiredSuiteSize,
-				XmaximumNumberOfTestSequences_to_try,
-				XT3suitedir + "/" + CUT + ".tr",
-				XDatadir + "/" + CUT + "_t3gen.txt") ;
-	}
-	
-	static void genSuiteMinsMaxs() throws Exception {
-		String CUT = "MinsMaxs" ;
-		generate(null,XCUTrootdir,
-				CUT,
-				"getMinsMaxs",
-				XdesiredSuiteSize,
-				XmaximumNumberOfTestSequences_to_try,
-				XT3suitedir + "/" + CUT + ".tr",
-				XDatadir + "/" + CUT + "_t3gen.txt") ;
-	}
 	
-
-
-	static public void main(String[] args) throws Exception {
-		//genSuiteTriangle() ;
-		genSuiteMinsMaxs() ;
-	}
 	
 }

experiments/wermer2/README.md

 ### Wermer experiment, version 2
 
-### To run the mutation test:
-
-- Compile the subjects using the script *./compileSubjects.sh*
-
-- Create mutation files using major. Script: *./generateMutants.sh <target>*. The target is the target name. e.g. Triangle. Without .java extension.
-
 
+### Folder structure:
 
-- Edit settings.hs to specify the post-condition and test file
-- Run the main function (this can be done using ghci)
-- The results will be stored in wlp/Results, overwriting any existing results file that uses the same parameters (the analysis is static, so the results should be the same in this case anyway)
+- `subjects` : contains the source code of the experiment subjects.
+- `tests` : contains manual and automated tests (t3-daikon) to be used as comparison.
+- `mutants` : contains the source code of the mutants of the subjects. Some mutants are generated (with Major); each such mutant injects an error (though it may turn out that the mutation is a non-error). Some mutants are manually crafted, these should all be non-error mutants, intended to check the wlp does indeed identify them as non-errors.
 
-### To run the false positive test:
+- `data` : contains raw data generated by the experiments.
+- `tmp`  : contains temporary artifacts such as log files generated by the experiments.
 
-- Edit settings.hs to specify the post-condition
-- Run the testFalsePositives function (this can be done using ghci)
-- The results will be stored in wlp/Results
+- `t3daikongen` : contains a Java program and related classes to generate t3 test suites and daikon invariants.
 
-### Folder structure:
+### Scripts and script-related artifacts
 
-The folder generated by Major must be in the same folder as the wlp folder, and must be named "SOURCE mutants" (where SOURCE is the name of the test class)
-A path to a mutant (the 5th mutant in this example) looks like this: "SOURCE mutants/5/classPath/SOURCE.java" Because of this, to analyse a new test class the classPath function in Settings.hs has to be extended with the corresponding class path
+- `WlpExperiment.hs` : a Haskell script to run the whole wlp-part of wermer experiments (only the wlp part!).
+- `generateMutans.hs` : to generate the source of code bug-injecting mutants. It uses Major, but does not do any mutation testing. The experiment folder should already contain these generated mutants so there should be no need to call this script again.
+- `mutation.mml` : the definition of the used mutation operators and targets. This is used by Major and `generateMutans.hs`.
+- `mutation.mml.bin` : compiled version of `mutation.mml`.
 

experiments/wermer2/build.xml

+<project name="Wermer2 Manual and Daikon mutation test" basedir=".">
+
+<!-- ##############################################
+    
+    You need to use Major's ant to run this build file: ../tools/major/bin/ant
+    
+          Path to Major and Mutation options 
+          Use -Dmutation="=mml-file" to set path to mml-file
+
+<property name="mutOp" value=":NONE"/>
+<property name="mutator" value="-XMutator${mutOp}"/>
+
+     ############################################## -->
+
+<property name="toolshome" value="../tools"/>
+
+<property name="mutator" value="-XMutator=./mutation.mml.bin"/>
+<property name="major" value="${toolshome}/major/bin/javac"/>
+
+
+<target name="init">
+   <mkdir dir="tmp/classes"/>
+ </target>
+ 
+<target name="clean">
+   <delete dir="tmp/classes"/>
+</target>   
+ 
+
+<!-- Target to compile the subjects using Major (which would already prepare the mutations) -->
+<target name="compile.subjects" depends="init" description="Compile">
+    <javac includeantruntime="true" 
+           srcdir="subjects/src"
+           destdir="tmp/classes"
+           debug="yes"
+           fork="yes"
+           executable="${major}">
+
+        <compilerarg value="${mutator}"/>
+    </javac>
+</target>
+
+<!-- Target to compile the test suite -->
+<target name="compile.tests" depends="compile.subjects" description="Compile all tests">
+    <javac includeantruntime="true" 
+           srcdir="tests/src"
+           classpath="tmp/classes;${toolshome}/junit.jar;${toolshome}/t3daikon;${toolshome}/t3daikon/T3.jar;${toolshome}/t3daikon/T3daikon.jar"
+           destdir="tmp/classes"
+           debug="yes">
+    </javac>
+</target>    
+              
+<!-- to run all the tests (manual and t3-daikon) -->                
+<target name="test" depends="compile.tests" description="Run all unit test cases">
+    <junit printsummary="true"
+           showoutput="true"
+           haltonfailure="true">
+           <formatter type="plain" usefile="true"/>
+           <classpath path="tmp/classes;${toolshome}/t3daikon;${toolshome}/t3daikon/T3.jar;${toolshome}/t3daikon/T3daikon.jar"/>
+           <batchtest fork="no">
+                <fileset dir="tests/src">
+                    <include name="**/*Test*.java"/>
+                </fileset>
+           </batchtest>
+    </junit>
+</target>
+    
+<property name="CUT" value="MinsMaxs"/>
+
+    
+<target name="mutation.test1" description="Run mutation analysis on a single target">
+    <echo message="Running mutation analysis on ${CUT} ..."/>
+    <junit printsummary="false"
+           showoutput="false"
+           mutationAnalysis="true"
+           summaryFile="data/${CUT}_bug_${MODE}Test_summary.csv"
+           resultFile="data/${CUT}_bug_${MODE}Test_results.csv"
+           killDetailsFile="data/${CUT}_bug_${MODE}Test_killed.csv">
+           <classpath path="tmp/classes;${toolshome}/t3daikon;${toolshome}/t3daikon/T3.jar;${toolshome}/t3daikon/T3daikon.jar"/>
+           <batchtest fork="false">
+               <fileset dir="tests/src">
+                   <include name="${MODE}Test${CUT}.java"/>
+               </fileset>
+           </batchtest>
+    </junit>
+</target>
+
+<target name="allmutation.test" description="Run mutation analysis on all targets">
+    <antcall target="mutation.test1">
+        <param name="CUT" value="Triangle"/>
+        <param name="MODE" value="Manual"/>
+    </antcall>
+    <antcall target="mutation.test1">
+        <param name="CUT" value="Triangle"/>
+        <param name="MODE" value="T3"/>
+    </antcall>
+    <antcall target="mutation.test1">
+        <param name="CUT" value="MinsMaxs"/>
+        <param name="MODE" value="Manual"/>
+    </antcall>
+    <antcall target="mutation.test1">
+        <param name="CUT" value="MinsMaxs"/>
+        <param name="MODE" value="T3"/>
+    </antcall>
+</target>
+
+
+</project>
\ No newline at end of file

experiments/wermer2/compileSubjects.sh

 #!/bin/bash  
 
 SRC="./subjects/src"
-SUBJECTS="$SRC/Triangle.java"
-javac -cp "./subjects/bin"  -d "./subjects/bin" $SUBJECTS
+DESTDIR="./subjects/compiled" 
+SUBJECTS="$SRC/Triangle.java $SRC/MinsMaxs.java"
+javac -cp "."  -d $DESTDIR $SUBJECTS
 

experiments/wermer2/t3daikongen/Generate_Suite_and_Invs.java

+import static Sequenic.T3.Generator.Value.ValueMGCombinators.*;
+
+import Sequenic.T3.Sequence.Datatype.*;
+
+public class Generate_Suite_and_Invs {
+	
+	public static String ExperimentHome = "/Users/iswbprasetya/workshop/projects/koenwlp/repo/javawlp/experiments/wermer2" ;
+	public static String XCUTrootdir = ExperimentHome + "/subjects/compiled" ;
+	public static String XDatadir = ExperimentHome + "/data" ;
+	public static String XT3suitedir = ExperimentHome + "/tests/t3suite" ;
+	
+	static int XdesiredSuiteSize = 1000 ;
+	static int XmaximumNumberOfTestSequences_to_try = 5000 ;
+	
+	static void genSuiteAndInvs(Sequenic.T3.Generator.Generator<PARAM,STEP> customgen,
+			String CUT,
+			String targetMethod) throws Exception 
+	{
+		SUITE S = MyT3.generate(customgen,XCUTrootdir,CUT,targetMethod,
+				       XdesiredSuiteSize,
+				       XmaximumNumberOfTestSequences_to_try,
+				       XT3suitedir + "/" + CUT + ".tr",
+				       XDatadir + "/" + CUT + "_t3gen.txt") ;
+		MyDaikonUtils.mineInvariants(S, targetMethod, XT3suitedir + "/" + CUT) ;
+	}
+	
+	static void genSuiteTriangle() throws Exception {
+		Sequenic.T3.Generator.Generator<PARAM,STEP> customgen = Float(OneOf(-2.1f,-1f,0f,0.01f,1f,1.1f,2f,3f,4.5f,9f)) ;
+		genSuiteAndInvs(customgen,"Triangle","tritype1") ;
+	}
+	
+	static void genSuiteMinsMaxs() throws Exception {
+		genSuiteAndInvs(null,"MinsMaxs","getMinsMaxs") ;
+	}
+	
+
+
+	static public void main(String[] args) throws Exception {
+		genSuiteTriangle() ;
+		genSuiteMinsMaxs() ;
+	}
+
+}

experiments/wermer2/tests/src/T3TestMinsMaxs.java

+import org.junit.* ;
+import static org.junit.Assert.assertTrue;;
+
+public class T3TestMinsMaxs {
+	@Test
+	public void test() throws Exception {
+		String CUT = "MinsMaxs" ;
+		String suitefile = XConf.XT3suitedir + "/" + CUT + ".tr" ;
+		String invfile = XConf.XT3suitedir + "/" + CUT + ".inv" ;
+		assertTrue(MyDaikonUtils.checkInvariants(suitefile,"getMinsMaxs",invfile)) ;
+	}
+}

experiments/wermer2/tests/src/T3TestTriangle.java

+import org.junit.* ;
+import static org.junit.Assert.assertTrue;;
+
+
+public class T3TestTriangle {
+	
+
+	
+	@Test
+	public void test() throws Exception {
+		String CUT = "Triangle" ;
+		String suitefile = XConf.XT3suitedir + "/" + CUT + ".tr" ;
+		String invfile   = XConf.XT3suitedir + "/" + CUT + ".inv" ;
+		assertTrue(MyDaikonUtils.checkInvariants(suitefile,"tritype1",invfile)) ;
+	}
+
+}

experiments/wermer2/tests/src/XConf.java

+
+public class XConf {
+	public static String ExperimentHome = "/Users/iswbprasetya/workshop/projects/koenwlp/repo/javawlp/experiments/wermer2" ;
+	public static String XT3suitedir = ExperimentHome + "/tests/t3suite" ;
+}

experiments/wermer2/tests/t3suite/MinsMaxs.inv.txt

+Daikon version 5.2.4, released May 1, 2015; http://plse.cs.washington.edu/daikon.
+Reading declaration files 
[1:45:15 PM]:                                                                  
                                                                               

                                                                               
Processing trace data; reading 1 dtrace file:
+[1:45:15 PM]: Finished reading /Users/iswbprasetya/workshop/projects/koenwlp/re
+                                                                               
The --output_num_samples debugging flag is on.
+Some of the debugging output may only make sense to Daikon programmers.
+===========================================================================
+getMinsMaxs(double[][]):::ENTER  1000 samples
+    Variables: arg0[] size(arg0[]) size(arg0[])-1
+arg0[] elements != null		(1000 samples)
+size(arg0[]) one of { 0, 1, 2 }		(1000 samples)
+===========================================================================
+getMinsMaxs(double[][]):::EXIT  1000 samples
+    Variables: arg0[] exception return[] orig(arg0[]) size(arg0[]) size(arg0[])-1 size(return[]) size(return[])-1 orig(size(arg0[])) orig(size(arg0[]))-1
+      Unmodified variables: arg0[] size(arg0[])
+arg0[] == orig(arg0[])		(1000 samples)
+arg0[] elements != null		(1000 samples)
+exception one of { "", "java.lang.IllegalArgumentException", "java.lang.NullPointerException" }		(1000 samples)
+return[] elements != null		(1000 samples)
+size(arg0[]) one of { 0, 1, 2 }		(1000 samples)
+size(return[]) one of { 0, 2 }		(1000 samples)
+size(return[])-1 != 0		(1000 samples)
+size(arg0[]) % size(return[])-1 == 0		(1000 samples)
+size(arg0[]) >= size(return[])-1		(1000 samples)
+size(arg0[])-1 != size(return[])		(1000 samples)
+size(arg0[])-1 % size(return[])-1 == 0		(1000 samples)
+===========================================================================
+Variables:
+  non_canonical_variables = 0
+  can_be_missing_variables = 0
+  canonical_variables = 0
+  total variables = 0
+Derivation:
+  derived_variables = 8
+  suppressed derived variables = 0
+    nonsensical_suppressed_derived_variables = 0
+    tautological_suppressed_derived_variables = 0
+Inference:
+Non-instantiated: 0
+  true = 0
+    implied_noninstantiated_invariants = 0
+    subexact_noninstantiated_invariants = 0
+  false = 0
+    implied_false_noninstantiated_invariants = 0
+    partially_implied_invariants = 0
+Instantiated: 275 = 212
+  falsified_invariants = 126
+  non_falsified_invariants = 86 = 14
+    unjustified = 0
+      too_few_samples_invariants = 0
+      unjustified_invariants = 0
+    implied = 0
+      non_canonical_invariants = 0
+      obvious_invariants = 0
+    reported_invariants = 14
+Exiting Daikon.