Add some tools and categories

_index.md

@@ -11,11 +11,11 @@ From decades-old classics to cutting-edge tools, this site aims to put as much i
 
 Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site). 
 
-{{<button href="/applications/smt-solver/">}}
+{{<button href="/tools">}}
-SMT Solvers
+List of Tools
 {{</button>}} 
-{{<button href="/applications/model-checker/">}}
+{{<button href="/taxonomies">}}
-Model Checkers
+Taxonomy Data
 {{</button>}} 
 {{<button href="/contribute">}}
 Contribute

tools/mc/_index.md

@@ -0,0 +1,10 @@
++++
+title = "Model Checking Tools"
+layout = "section"
++++
+
+This page lists all of the model checking tools on this site in alphabetical order.
+Click a tool name in the first column to view tool details. 
+Click a colorful item in the second column to view all the tools for which that term applies.
+Item colors mean nothing and are intended to make it easy to skim the page. 
+Colors are generated by hashing each term's name and converting it to RGB color values.

tools/mc/sally.md

@@ -0,0 +1,24 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Sally'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "http://sri-csl.github.io/sally/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/SRI-CSL/sally", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Model Checker']
+developers = ['SRI International']
+licenses = ['GPLv2']
+inputs = ['Sally']
+interfaces = ['CLI']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+# publications = ['']
++++
+
+<!-- {{<inactive year="2023">}} -->
+
+
+Sally is a model checker for infinite state systems described as transition systems.

tools/pmc/stamina.md

@@ -1,22 +0,0 @@
-+++
-date = 2025-06-07
-draft = true
-title = 'STAMINA TODO'
-subtitle = 'Probabilistic Model Checker'
-links = [
-    { title = "Homepage", url = "https://cvc5.github.io/", icon = 'fa-solid fa-home' },
-    { title = "Source Code", url = "https://github.com/dreal/dreal4", icon = 'fa-brands fa-github'  },
-    { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
-]
-applications = ['Probabilistic Model Checker', 'Rare Events']
-developers = ['Utah State University']
-licenses = ['BSD']
-inputs = ['SMTLIB2']
-interfaces = ['CLI', 'Online']
-maintenance = ['Actively Maintained']
-# techniques = ['CDCL']
-publications = ['Barbosa2022']
-+++
-
-<!-- {{<inactive year="2023">}} -->
-cvc5 is an automatic theorem prover for SMT problems.

tools/prob/_index.md

@@ -1,9 +1,9 @@
 +++
-title = "All PMC Tools"
+title = "Probabilistic Tools"
 layout = "section"
 +++
 
-This page lists all of the SAT & SMT tools on this site in alphabetical order.
+This page lists all of the probabilistic tools on this site in alphabetical order.
 Click a tool name in the first column to view tool details. 
 Click a colorful item in the second column to view all the tools for which that term applies.
 Item colors mean nothing and are intended to make it easy to skim the page. 

tools/prob/prism.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'PRISM'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://prismmodelchecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/prismmodelchecker/prism", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Oxford University']
+licenses = ['GPLv2']
+inputs = ['PRISM', 'MRMC']
+interfaces = ['CLI', 'Java']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Kwiatkowska2011']
++++
+
+<!-- {{<inactive year="2023">}} -->
+PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.

tools/prob/stamina.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'STAMINA'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://staminachecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://staminachecker.org/source.html", icon = 'fa-brands fa-github'  },
+    { title = "Playground", url = "https://staminachecker.org/run.html", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['Utah State University']
+licenses = ['MIT', 'GPLv3']
+inputs = ['PRISM']
+interfaces = ['CLI', 'Online']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Jeppson2023']
++++
+
+<!-- {{<inactive year="2023">}} -->
+ A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either [Storm](../storm) or [PRISM](../prism).

tools/prob/storm.md

@@ -0,0 +1,22 @@
++++
+date = 2025-06-07
+draft = false
+title = 'Storm'
+subtitle = 'Probabilistic Model Checker'
+links = [
+    { title = "Homepage", url = "https://www.stormchecker.org/", icon = 'fa-solid fa-home' },
+    { title = "Source Code", url = "https://github.com/moves-rwth/storm", icon = 'fa-brands fa-github'  },
+    # { title = "Playground", url = "https://cvc5.github.io/app/", icon = 'fa-solid fa-gamepad' }
+]
+applications = ['Probabilistic Model Checker']
+developers = ['RWTH Aachen']
+licenses = ['GPLv3']
+inputs = ['PRISM', 'JANI', 'PNML', 'GreatSPN', 'Galileo', 'MRMC']
+interfaces = ['CLI', 'C++', 'Python']
+maintenance = ['Actively Maintained']
+# techniques = ['CDCL']
+publications = ['Hensel2022']
++++
+
+<!-- {{<inactive year="2023">}} -->
+Storm is a tool for the analysis of systems involving random or probabilistic phenomena. 

tools/sat-smt/_index.md

@@ -1,5 +1,5 @@
 +++
-title = "All SAT & SMT Tools"
+title = "SAT & SMT Tools"
 layout = "section"
 +++
 

tools/sat-smt/lingeling.md

@@ -2,7 +2,7 @@
 date = 2025-06-07
 draft = false
 title = 'Lingeling'
-subtitle = 'SMT Solver'
+subtitle = 'SAT Solver'
 links = [
     { title = "Homepage", url = "https://fmv.jku.at/lingeling/", icon = 'fa-solid fa-home' },
     { title = "Source Code", url = "https://github.com/arminbiere/lingeling", icon = 'fa-brands fa-github'  },

tools/termination/_index.md

@@ -1,5 +1,5 @@
 +++
-title = "All Termination Tools"
+title = "Termination Tools"
 layout = "section"
 +++