Add links to webinterface (#610)

trunk/source/WebsiteStatic/config/tool_pages/automata_library.html

@@ -18,7 +18,7 @@ <h1>Automata Library</h1>
 
 
 <h2>Web Interface</h2>
-<p>The library is available via a web interface.
+<p>The library is available via a <a href="?ui=int&tool=automata_library">web interface</a>.
 We devised a small script language called <i>Automata Script</i> that allows to define automata and specify operations that should be performed.
 You can find several sample files in the web interface.</p>
 

trunk/source/WebsiteStatic/config/tool_pages/automizer.html

@@ -40,7 +40,7 @@ <h2>Awards</h2>
 <h2>Web Interface</h2>
 <p>
     <span style="font-variant: small-caps">Ultimate</span> Automizer is
-    available via a web interface in which you can verify C programs.
+    available via a <a href="?ui=int&tool=automizer">web interface</a> in which you can verify C programs.
 </p>
 
 <h2>Download</h2>

trunk/source/WebsiteStatic/config/tool_pages/buechi_automizer.html

@@ -13,7 +13,7 @@ <h1>Büchi Automizer</h1>
 </p>
 
 <h2>Web Interface</h2>
-<p> <span style="font-variant:small-caps">Ultimate</span> Automizer is available via a web interface in which you can analyse termination of C programs. This version has some limitations. We use a theorem prover that does not support non-linear arithmetic and therefore the built-in tool <a href="http://ultimate.informatik.uni-freiburg.de/LassoRanker">LassoRanker</a> can only provide linear ranking functions.</p>
+<p> <span style="font-variant:small-caps">Ultimate</span> Automizer is available via a <a href="?ui=int&tool=buechi_automizer">web interface</a> in which you can analyse termination of C programs. This version has some limitations. We use a theorem prover that does not support non-linear arithmetic and therefore the built-in tool <a href="http://ultimate.informatik.uni-freiburg.de/LassoRanker">LassoRanker</a> can only provide linear ranking functions.</p>
 
 <h2>Commandline Version</h2>
 <p>Ultimate Büchi Automizer and the built-in tool <a href="http://ultimate.informatik.uni-freiburg.de/LassoRanker">LassoRanker</a> are in heavy development. A recent version is available on request, please contact <a href="http://swt.informatik.uni-freiburg.de/staff/heizmann">Matthias Heizmann</a>.</p>

trunk/source/WebsiteStatic/config/tool_pages/eliminator.html

@@ -27,7 +27,7 @@ <h1>Eliminator</h1>
 
 
 <h2>Web Interface</h2>
-<p><span style="font-variant:small-caps">Ultimate Eliminator</span> is available via a web interface.
+<p><span style="font-variant:small-caps">Ultimate Eliminator</span> is available via a <a href="?ui=int&tool=eliminator">web interface</a>.
 In this web interface <span style="font-variant:small-caps">Ultimate Eliminator</span> wraps the <a href="https://ultimate.informatik.uni-freiburg.de/smtinterpol">SMTInterpol</a> SMT solver.
 </p>
 

trunk/source/WebsiteStatic/config/tool_pages/kojak.html

@@ -8,7 +8,7 @@ <h1>Kojak</h1>
 	<h2>Web interface</h2>
 	<p>
 		<span style="font-variant: small-caps">Ultimate</span> Kojak is
-		available via a web interface.
+		available via a <a href="?ui=int&tool=kojak">web interface</a>.
 	</p>
 
 

trunk/source/WebsiteStatic/config/tool_pages/lasso_ranker.html

@@ -74,7 +74,7 @@ <h2>Web Interface</h2>
 
 <p>
 <span style="font-variant:small-caps">Ultimate LassoRanker</span> is available via a
-web interface. This web interface allows `playing around' with lasso programs written C or the <a href="http://research.microsoft.com/en-us/projects/boogie/">Boogie</a> intermediate verification language.
+<a href="?ui=int&tool=lasso_ranker">web interface</a>. This web interface allows `playing around' with lasso programs written C or the <a href="http://research.microsoft.com/en-us/projects/boogie/">Boogie</a> intermediate verification language.
 </p>
 
 

trunk/source/WebsiteStatic/config/tool_pages/ltl_automizer.html

@@ -6,7 +6,7 @@ <h1>LTL Automizer</h1>
 </p>
 
 <h2>Web interface</h2>
-<p><span style="font-variant:small-caps">Ultimate LTL Automizer</span> is available via a web interface.</p>
+<p><span style="font-variant:small-caps">Ultimate LTL Automizer</span> is available via a <a href="?ui=int&tool=ltl_automizer">web interface</a>.</p>
 
 <h2>CAV 2015 Submission "Fairness Modulo Theory: A New Approach to LTL Software Model Checking"</h2>
 <h3>Extended version of the paper</h3>

trunk/source/WebsiteStatic/config/tool_pages/perti_automizer.html

@@ -5,7 +5,7 @@ <h1>Petri Automizer</h1>
 	<p>Ultimate Petri Automizer implements a Petri net-based approach for the verification of concurrent programs.</p>
 
 <h2>Web Interface</h2>
-<p><span style="font-variant:small-caps">Petri Automizer</span> is available via a web interface.</p>
+<p><span style="font-variant:small-caps">Petri Automizer</span> is available via a <a href="?ui=int&tool=perti_automizer">web interface</a>.</p>
 
 </body>
 </html>

trunk/source/WebsiteStatic/config/tool_pages/referee.html

@@ -5,7 +5,7 @@ <h1>Referee</h1>
 	<p>Ultimate Referee checks given invariants.</p>
 
 <h2>Web Interface</h2>
-<p><span style="font-variant:small-caps">Referee</span> is available via a web interface.</p>
+<p><span style="font-variant:small-caps">Referee</span> is available via a <a href="?ui=int&tool=referee">web interface</a>.</p>
 
 </body>
 </html>

trunk/source/WebsiteStatic/config/tool_pages/taipan.html

@@ -8,7 +8,7 @@ <h1>Taipan</h1>
 	<h2>Web interface</h2>
 	<p>
 		<span style="font-variant: small-caps">Ultimate</span> Taipan is
-		available via a web interface.
+		available via a <a href="?ui=int&tool=taipan">web interface</a>.
 	</p>