Switch branches/tags
Find file History
jon-jacky add commands tdiff and tclean
tdiff is the new name for clogdiff (which is retained but now deprecated)
trun is revised, add tdiff and tclean to MANIFEST.in and bin/README.md too
revisions still needed in notes/test.txt etc.
Latest commit a0da67c May 10, 2013
Permalink
..
Failed to load latest commit information.
fsmpy a few more files in fsmpy/ and svg/ directories Feb 21, 2013
svg a few more files in fsmpy/ and svg/ directories Feb 21, 2013
testsuite samples: commit test output files Nov 21, 2012
OneUserDomain.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
OneUserFilter.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
OneUserNoIntScenario.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
OneUserScenario.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
PHPLocalConfig.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
README.md fix pmt.py -o offline test gen. option Mar 31, 2013
ScenarioLogin.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
Session.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
Stepper.py WebApplication Stepper.py: fix port number in default URL Mar 29, 2013
TestIntFailure.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestIntSuccess.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestIntSuccessNoNone.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestIntTwoRuns.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestIntTwoUsers.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestIntWrong.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestIntWrongLogout.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
TestLoginFiveFailures.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
VerboseConfig.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
WSGIVerboseConfig.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
WebModel.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
local8080config.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
nmodelconfig.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
test.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test.ref WebApplication/test*.ref: more output Nov 19, 2012
test_composition.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_composition.ref WebApplication/test*.ref: more output Nov 19, 2012
test_e_testsuite.py Now -e and -a options work with TestSuite Dec 7, 2012
test_e_testsuite.ref revise test scripts, regenerate .ref files of expected test output May 1, 2013
test_graphics.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_graphics.ref WebApplication tests: regenerate .ref files Nov 19, 2012
test_ls.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
test_no_composition.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_no_composition.ref WebApplication/test*.ref: more output Nov 19, 2012
test_offline.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_offline.ref revise test scripts, regenerate .ref files of expected test output May 1, 2013
test_scenarios.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_scenarios.ref WebApplication/test*.ref: more output Nov 19, 2012
test_stepper.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_stepper.ref first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011
test_validation.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
test_validation.ref WebApplication tests: regenerate .ref files Nov 19, 2012
webapp.py add pma etc. in bin directory, run pma.py etc. in pymodel Apr 10, 2013
wsgiconfig.py first git commit from svn pymodel trunk, same as svn pymodel-0.9 tag Jul 12, 2011

README.md

WebApplication

This sample contains WebModel, a model for a web application, webapp, an actual web application implementation (in Python), and Stepper, a stepper that allows the tester pmt to use the model to drive the web application.

The web application has a bug -- it doesn't conform to the model.

Start the web application on localhost at port 8000: wsgirunner webapp. Use the -p option to use a different port: wsgirunner -p 8080 webapp To stop the web application, type ^C in the terminal window where you started it, or close the window.

To see the web application running, point a browser at http://localhost:8000/webapp.py (or whatever port you chose). At Username: enter user1 (or user2), at Password: enter 123 (or 234), then click Submit.

On successful login, the web application displays a data page that shows a number, a string, and forms to enter a new value for each. Enter and submit some new values; the page updates to show the most recent entries. Select the Log out link, the application shows a blank page.

Enter the original webapp.py URL into the browser to log in as the same user again. The data page appears, showing the string you entered during the last session, but the number zero. This is the bug: the web application is supposed to store both the string and number entered by each user, and persist them from one login session to the next, but it fails to store the number.

Stepper is a web client. It simulates a browser, sending HTTP requests to the web application. It uses the urllib, urllib2, and cookielib modules from the Python standard library.

By default, Stepper accesses http://localhost:8000/webapp.py. Alternatively, Stepper can use an optional Config module to select a different URL, or to select other options, such as printing out incoming HTTP requests. The sample includes several configuration modules: WSGIVerboseConfig etc. To use one, copy it (or symlink it) to Config.py.

The only test script that uses Stepper is test_stepper. To run this test, you must first start the web application.

The rest of the test scripts only execute the model, so they do not need the web application to be running: test, test_graphics, and several others.

The modules are:

  • WebModel: model program for the web application

  • webapp: web application (implementation)

  • Stepper: enables pmt to use WebModel (etc.) to drive webapp

  • WSGIVerboseConfig, wsgiconfig, PHPLocalConfig, local8080config, VerboseConfig, nmodelconfig: configuration modules for Stepper that select different URLs for the web application, or other options such as printing the HTTP headers.

  • OneUserDomain: configuration for WebModel, limits users domain to one particular element

  • OneUserFilter: configuration for WebModel, assigns StateFilter to allow only one particular logged in user

  • OneUserScenario: scenario machine (FSM), compose with WebModel to allow only one particular user to log in and log out

  • OneUserNoIntScenario: scenario machine (FSM), compose with WebModel to allow only one particular user to log in and log out and to suppress the UpdateInt and ReadInt actions

  • ScenarioLogin: test suite, compose with WebModel to allow only one particular user to log in and log out

  • TestIntFailure, TestIntSuccess, TestIntSuccessNoNone, TestIntTwoRuns, TestIntTwoUsers, TestIntWrong, TestIntWrongLogout, TestLoginFiveFailures: test suites, use as offline tests

  • test: use pmt to generate traces from WebModel, with many test cases that demonstrate various pmt options and the built-in ActionNameCoverage and StateCoverage strategies. Also, one test case that executes the TestIntTwoRuns test suite.

  • test_offline: uses the pmt -o option to generate an offline test suite. The test_offline module contains instructions for running the generated tests.

  • test_scenarios - use pmt to generate traces from ScenarioLogin, OneUserScenario, and both composed with WebModel

  • test_stepper: test script that invokes pmt using Stepper to drive the web application webapp. The script includes test cases that do on-the-fly testing with WebModel and offline tests with TestIntSuccess, TestIntFailure, TestIntTwoFailures, and TestLoginFiveFailures. Test failures that indicate ended in non-accepting state are expected; repeating those commands with the pmt -c 1 option will cause them to succeed. Failures that indicate found 0 in page, expected 1 are caused by the persistence bug in the web application. (This is the only sample that uses Stepper and webapp.)

  • test_graphics: generate graphs from WebModel, OneUserDomain, OneUserScenario, OneUserFilter, and OneUserNoIntScenario, alone and in combination

  • test_validation - generate graphs of the test suites TestIntSuccess and TestIntWrong, alone and composed with WebModel

  • test_no_composition: generates graphs from the test suite TestIntSuccess, the FSM OneUserScenario, and the model program WebModel

  • test_composition: generate graphs from TestIntSuccess, TestIntWrong, their composition TestIntSuccess x TestIntWrong, and the composition TestIntSuccess x TestIntWrongLongout

  • test_e_testsuite: - generate graphs from TestIntTwoRuns, demonstrates the pmv -e, -a, and -o options

  • test_ls: show you can run any program in a test script, not just PyModel programs

  • fsmpy, svg: directories of output files from test_graphics or test_viewer

View the generated graphics files in a browser. Hover the pointer over any state bubble to see a tooltip that shows the state variables in that state.

  • WebModelFSM: graph generated by exploring WebModel alone, limited only by the pma -m 50 option (to limit the number of transitions). Exploration stopped at all the states colored orange.

  • OneUserScenario, OneUserNoIntScenario: scenario machines (FSMs) for composing with WebModel

  • OneUserScenarioFSM, OneUserNoIntScenarioFSM, OneUserFilterFSM, OneUserDomainFSM: graphs generated from WebModel combined with other modules that restrict its behavior.

  • TestIntWrongLogoutFSM, TestIntWrongFSM, TestIntTwoRuns_NoLogout, TwoIntTwoRuns_Add, TestIntTwoRunsFSM, TestIntSuccessFSM, TestIntFailureFSM: graphs of test suites including traces that are forbidden by the model. They all reach their own accepting states, which are colored green.

  • TestWrongComposeFSM, TestSuccessComposeFSM, TestComposeLogoutFSM, TestIntComposeFSM: graphs of tests suites composed with the model. Each trace ends in the last state allowed by the model. If this is not the last state in the trace from the test suite, it is colored yellow. This indicates that the trace is not allowed by the model. If the whole trace is allowed by the model, the last state is green.

Revised Mar 2013