diff --git a/org.lamport.tla.toolbox.doc/html/cloudtlc/index.html b/org.lamport.tla.toolbox.doc/html/cloudtlc/index.html index 57ad2ea7dda7ec16a934b383877016f6090a9dec..422635bd70b426180390a3e90fde5f2e3ea0a21f 100644 --- a/org.lamport.tla.toolbox.doc/html/cloudtlc/index.html +++ b/org.lamport.tla.toolbox.doc/html/cloudtlc/index.html @@ -259,85 +259,96 @@ Figure 11 Final result loaded </li> </ol> + + <h1 class="Section"> <a class="toc" name="toc-Section-5">5</a> Common problems </h1> -<ul> -<li> -The Toolbox fails to start the cloud instance<ul> -<li> -Re-check your credentials -</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. -</li> - -</ul> - -<li> -The cloud instance sends "system notification" emails warning that the remaining disc space is at a critical level:<br> - <i>"tlc :: tlc :: Disk usage in percent<br> - CRITICALs: / is 92.23..."</i> <ul> -<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. -<ul> -<li> -<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> -# Download a jmx commandline client<br> + <li> + The Toolbox fails to start the cloud instance + <ul> + <li> + Re-check your credentials + </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. + </li> + </ul> + </li> + + <li> + The cloud instance sends "system notification" emails warning that the remaining disc space is at a critical level: + <pre class="listing"> + <i>"tlc :: tlc :: Disk usage in percent + CRITICALs: / is 92.23..."</i> + </pre> + <ul> + <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. + <ul> + <li> + <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> + <pre class="listing"> +# Download a jmx commandline client wget http://crawler.archive.org/cmdline-jmxclient/cmdline-jmxclient-0.10.3.jar -</li> -<li> -# Connect to the locally running TLC and have it create a checkpoint<br> + </pre> + </li> + <li> + <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 -</li> -<li> -Re-attach to the screen session running TLC and terminate TLC wth CTRL^C -</li> -<li> -# Restart TLC and have it recover from the checkpoint created<br> + </pre> + </li> + <li> + Re-attach to the screen session running TLC and terminate TLC wth CTRL^C + </li> + <li> + <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/ -</li> -</ul> - -</li> + </pre> + </li> + </ul> + </li> + </ul> + </li> + <ul> + <li> + The cloud instance sends "system notification" email warnings directly after startup. + <ul> + <li> + Ignore these emails :-). + </li> + <li> + This happens primarily on Azure when the monitoring runs too earlier before the cloud instance is fully started. + </li> + </ul> + </li> + <li> + The runtime statistics (web browser) indicate that TLC has finished model checking, but no result is sent via email. + <ul> + <li> + Check your email spam folder if the model checking result has incorrectly been classified as spam + </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. + </li> + <ul> + <li> + Copy & 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> + </ul> + </ul> + </li> + </ul> </ul> -<li> -The cloud instance sends "system notification" email warnings directly after startup. -<ul> -<li> -Ignore these emails :-). -</li> -<li> -This happens primarily on Azure when the monitoring runs too earlier before the cloud instance is fully started. -</li> -</ul> -</li> -<li> -The runtime statistics (web browser) indicate that TLC has finished model checking, but no result is sent via email.<ul> -<li> -Check your email spam folder if the model checking result has incorrectly been classified as spam -</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> -<li> -Copy & 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> - -</ul> - -</li> - -</ul> -</li> - -</ul> </div> </body>