Tex2Smv

Tex2Smv

Translating Latex code to SMV code

Background

NuSMV is a tool for formal verification using LTL, CTL and StateCharts. It's input language consists of symbols like "|", "&", "!", "G", "F" etc.
Latex is a language for writing scientific texts. The corresponding symbols in it for the above are "\vee", "\wedge", "\neg", "\Box", "\Diamond".
If you are writing a Latex document that contains formulas of LTL or CTL, this small tool will translate those formula to the input language of NuSMV.

Usage

Input: a .tex file containing some CTL or LTL formulas. The file may contain other information as well.
Output: a .txt file containing several linex. Each line is a translation of a formula from the latex file to NuSMV input language.
The output file is saved in the input file's directory.
Execution:
- Download the jar file.
- Go to the directory of the downloaded jar file.
- Run "java -jar Tex2Smv.jar "

Example

Input File: tex2smv_example.tex
Command Line: java -jar Tex2Smv.jar tex2smv_example.tex
Output File: tex2smv_example.tex.txt

Downloads

Executable jar file: tex2smv.jar
Source: Tex2Smv.java, SmvUtils.java

Go back to my homepage