Skip to content
Snippets Groups Projects
Commit 84b95836 authored by Markus Alexander Kuppe's avatar Markus Alexander Kuppe
Browse files

Fix SAX parser errors caused by unmatched li & ul tags.

[Bug][Toolbox]
parent 37dfaff1
No related branches found
No related tags found
No related merge requests found
...@@ -259,26 +259,31 @@ Figure 11 Final result loaded ...@@ -259,26 +259,31 @@ Figure 11 Final result loaded
</li> </li>
</ol> </ol>
<h1 class="Section"> <h1 class="Section">
<a class="toc" name="toc-Section-5">5</a> Common problems <a class="toc" name="toc-Section-5">5</a> Common problems
</h1> </h1>
<ul> <ul>
<li> <li>
The Toolbox fails to start the cloud instance<ul> The Toolbox fails to start the cloud instance
<ul>
<li> <li>
Re-check your credentials Re-check your credentials
</li> </li>
<li> <li>
If your credentials are correct, please turn on debug logging (start the Toolbox executable with “toolbox -console -consolelog”) and send us the output. You might have encountered a bug in cloud based distributed TLC. If your credentials are correct, please turn on debug logging (start the Toolbox executable with “toolbox -console -consolelog”) and send us the output. You might have encountered a bug in cloud based distributed TLC.
</li> </li>
</ul> </ul>
</li>
<li> <li>
The cloud instance sends "system notification" emails warning that the remaining disc space is at a critical level:<br> The cloud instance sends "system notification" emails warning that the remaining disc space is at a critical level:
<i>"tlc :: tlc :: Disk usage in percent<br> <pre class="listing">
<i>"tlc :: tlc :: Disk usage in percent
CRITICALs: / is 92.23..."</i> CRITICALs: / is 92.23..."</i>
</pre>
<ul> <ul>
<li> <li>
A long running TLC process writes unexplored states to the system disk for later exploration. With very large models, this can potentially use up all of the available disk space. If this happens, TLC will crash. Thus, if you received such a warning, please create a checkpoint, <a class="URL" href="http://docs.aws.amazon.com/AWSEC2/latest/UserGuide/ec2-add-volume-to-instance.html">attach a larger disk to your VM</a> and continue TLC by recovering from the checkpoint. A long running TLC process writes unexplored states to the system disk for later exploration. With very large models, this can potentially use up all of the available disk space. If this happens, TLC will crash. Thus, if you received such a warning, please create a checkpoint, <a class="URL" href="http://docs.aws.amazon.com/AWSEC2/latest/UserGuide/ec2-add-volume-to-instance.html">attach a larger disk to your VM</a> and continue TLC by recovering from the checkpoint.
...@@ -287,25 +292,31 @@ A long running TLC process writes unexplored states to the system disk for later ...@@ -287,25 +292,31 @@ A long running TLC process writes unexplored states to the system disk for later
<a class="URL" href="http://docs.aws.amazon.com/AWSEC2/latest/UserGuide/ec2-connect-to-instance-linux.html#using-putty">Connect to the cloud instance with ssh</a> <a class="URL" href="http://docs.aws.amazon.com/AWSEC2/latest/UserGuide/ec2-connect-to-instance-linux.html#using-putty">Connect to the cloud instance with ssh</a>
</li> </li>
<li> <li>
# Download a jmx commandline client<br> <pre class="listing">
# Download a jmx commandline client
wget http://crawler.archive.org/cmdline-jmxclient/cmdline-jmxclient-0.10.3.jar wget http://crawler.archive.org/cmdline-jmxclient/cmdline-jmxclient-0.10.3.jar
</pre>
</li> </li>
<li> <li>
# Connect to the locally running TLC and have it create a checkpoint<br> <pre class="listing">
# Connect to the locally running TLC and have it create a checkpoint
java -jar cmdline-jmxclient-0.10.3.jar - localhost:5400 tlc2.tool:type=ModelChecker checkpoint java -jar cmdline-jmxclient-0.10.3.jar - localhost:5400 tlc2.tool:type=ModelChecker checkpoint
</pre>
</li> </li>
<li> <li>
Re-attach to the screen session running TLC and terminate TLC wth CTRL^C Re-attach to the screen session running TLC and terminate TLC wth CTRL^C
</li> </li>
<li> <li>
# Restart TLC and have it recover from the checkpoint created<br> <pre class="listing">
# Restart TLC and have it recover from the checkpoint created
java -jar tla2tools.jar -recover /path/to/states/15-12-16-12-16-04/ java -jar tla2tools.jar -recover /path/to/states/15-12-16-12-16-04/
</pre>
</li> </li>
</ul> </ul>
</li> </li>
</ul> </ul>
</li>
<ul>
<li> <li>
The cloud instance sends "system notification" email warnings directly after startup. The cloud instance sends "system notification" email warnings directly after startup.
<ul> <ul>
...@@ -317,27 +328,27 @@ This happens primarily on Azure when the monitoring runs too earlier before the ...@@ -317,27 +328,27 @@ This happens primarily on Azure when the monitoring runs too earlier before the
</li> </li>
</ul> </ul>
</li> </li>
<li> <li>
The runtime statistics (web browser) indicate that TLC has finished model checking, but no result is sent via email.<ul> The runtime statistics (web browser) indicate that TLC has finished model checking, but no result is sent via email.
<ul>
<li> <li>
Check your email spam folder if the model checking result has incorrectly been classified as spam Check your email spam folder if the model checking result has incorrectly been classified as spam
</li> </li>
<li> <li>
Another reason why mail delivery might fail, are too strict spam counter measures at the mail server level. You might want to try to use a different email address (domain part) in the future. For Azure, it works best to use an Outlook.com email address.<ul> Another reason why mail delivery might fail, are too strict spam counter measures at the mail server level. You might want to try to use a different email address (domain part) in the future. For Azure, it works best to use an Outlook.com email address.
</li>
<ul>
<li> <li>
Copy &amp; paste the MC.out content from the browser window into a plain text file and load it from there (see <a class="Reference" href="#enu:Import-the-MC.out">4↑</a>) Copy &amp; paste the MC.out content from the browser window into a plain text file and load it from there (see <a class="Reference" href="#enu:Import-the-MC.out">4↑</a>)
</li> </li>
</ul> </ul>
</ul>
</li> </li>
</ul>
</ul> </ul>
</li>
</ul>
</div> </div>
</body> </body>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment