updating README

README.md

@@ -8,7 +8,7 @@ Yin-Yang is a tool for automatically stress-testing Satisfiability Modulo Theory
 
 - **Type-Aware Operator Mutation** [OOPSLA '20] mutates operators within SMT-LIB formulas and differentially tests two or more SMT solvers for inconsistent results.
 
-- **Semantic Fusion** [PLDI '20] is a metamorphic testing approach that generates an equisatisifiable formulas by fusing test seeds pairs of the same satisifiablity to stress test one or more SMT solvers.
+- **Semantic Fusion** [PLDI '20] is a metamorphic testing approach that generates an equisatisfiable formulas by fusing test seeds pairs of the same satisfiability to stress test one or more SMT solvers.
 
 
 
@@ -22,7 +22,7 @@ Requirements:
 
 The following commands clone Yin-Yang and install the antlr4 python runtime: 
 ```
-git clone https://github.com/wintered/yinyang.git
+git clone https://github.com/testsmt/yinyang.git 
 pip3 install antlr4-python3-runtime  
 ```
 
@@ -35,30 +35,30 @@ configuration, see [documentation.md](./docs/documentation.md).
 
 #### Type-Aware Operator Mutation
 ```
-python yinyang.py "<solver_clis>" <seed>
+python3 yinyang.py "<solver_clis>" <seed>
 ```
 where
 
-* `<solver_clis>`: a sequence of command line interfaces to call SMT solvers splitted by semicola `;`. Note that at least two SMT solvers are neccessary for differential testing.
+* `<solver_clis>`: a sequence of command line interfaces to call SMT solvers splitted by semicola `;`. Note that at least two SMT solvers are necessary for differential testing.
 
 
 * `<seed>`: an SMT-LIB v2.6 file
 
 Example:
 ```
-python yinyang.py "z3;cvc4 -q" examples/formulas/phi1.smt2 
+python3 yinyang.py "z3;cvc4 -q" examples/formulas/phi1.smt2 
 ```
-Yin-Yang will run *Type-Aware Operator Mutation* and generate 300 mutations on the seed for stress-testing z3 and cvc4. The expected behaviour of Yin-Yang is to output anything to stdout unless an error occurred (e.g. one of the solver cils is incorrect) or a bug has been found. If a bug has been found, the bug trigger is stored in `./bugs`.
+Yin-Yang will run *Type-Aware Operator Mutation* and generate 300 mutations on the seed for stress-testing z3 and cvc4. The expected behaviour of Yin-Yang is to output anything to stdout unless an error occurred (e.g. one of the solver clis is incorrect) or a bug has been found. If a bug has been found, the bug trigger is stored in `./bugs`.
 
 #### Semantic Fusion 
 
 ```
-python yinyang.py "<solver_clis>" -o <oracle> -s fusion <seed1> <seed2>
+python3 yinyang.py "<solver_clis>" -o <oracle> -s fusion <seed1> <seed2>
 ```
 
 where
 
-* `<solver_clis>`: a sequence of command line interfaces to call SMT solvers splitted by semicola `;`. Note, since Semantic Fusion is a metamorphic testing approach, one SMT solver is sufficient.
+* `<solver_clis>`: a sequence of command line interfaces to call SMT solvers separated by semicola `;`. Note, since Semantic Fusion is a metamorphic testing approach, one SMT solver is sufficient.
 
 * `<oracle>`: desired test oracle result {sat, unsat}.
 
@@ -68,9 +68,9 @@ where
 Example: 
 
 ```
-python yinyang.py "z3" -o sat -s fusion examples/formulas/formula1.smt2 examples/formulas/formula2.smt2 
+python3 yinyang.py "z3" -o sat -s fusion examples/formulas/phi1.smt2 examples/formulas/phi2.smt2 
 ```
-Yin-Yang will test z3 by running *Semantic Fusion* with 30 iterations on the two satisifiable seed formulas. Note, the mutants generated by Yin-Yang will then be by construction also be satisifable.
+Yin-Yang will test z3 by running *Semantic Fusion* with 30 iterations on the two satisfiable seed formulas. Note, the mutants generated by Yin-Yang will then be by construction also be satisfiable.
 
 
 Test Seeds & Limitations
@@ -80,7 +80,7 @@ SMT-LIB test seeds can be conveniently obtained via the following [script](http:
 Yin-Yang's parser supports the SMT-LIB v2.6 standard and so it is able to parse existing SMT-LIB.
 *Type-Aware Operator Mutation* can be used for formulas as any logic while *Semantic Fusion* currently only supports LIA, LRA, NRA, QF_LIA, QF_LRA, QF_NRA, QF_SLIA, QF_S logics in the non-incremental mode. To apply Semantic Fusion, test seeds
 Support for other logics is experimental; we are actively working on it. For *Semantic Fusion*, the seeds need to be pre-processed to separate them into 
-satisifable and unsatisfiable formulas. Pre-categorized are available in the following [repository](https://github.com/testsmt/semantic-fusion-seeds) 
+satisfiable and unsatisfiable formulas. Pre-categorized are available in the following [repository](https://github.com/testsmt/semantic-fusion-seeds) 
 
 Yin-Yang may also not be able to parse some non-standard .smt2 files such as, e.g., some files from the regression test suites of Z3 and CVC4. We are working on an extension of the parser to support such files.     
 
@@ -119,7 +119,7 @@ The testing approaches implemented in Yin-Yang are based on following two papers
 ## Comparing against Yin-Yang 
 The testing approaches within Yin-Yang are slightly different from the research prototypes used for these publications. If you want to compare against either one of them, please contact us to provide you with these prototypes and the configurations  used.
 
-Contributers                                                                       
+Contributors                                                                       
 ------------                          
 * [Dominik Winterer](https://wintered.github.io/) (primary maintainer) - [email protected]