From b59acc6ac631d3e4624b81867296812fcc9ff575 Mon Sep 17 00:00:00 2001 From: Jeanderson Candido Date: Wed, 20 Jun 2018 00:32:36 -0300 Subject: [PATCH] Removed docs dir (should be in a different place/branch) --- docs/graphics/DFSListener.svg | 3 --- docs/graphics/app-types.svg | 3 --- docs/graphics/attributes.svg | 3 --- docs/graphics/bc-factory.svg | 3 --- docs/graphics/cg-impl.svg | 3 --- docs/graphics/cg-motivation.svg | 3 --- docs/graphics/cg-ontology.svg | 3 --- docs/graphics/cg-sequence.svg | 3 --- docs/graphics/choicegen-example.svg | 3 --- docs/graphics/genpeer.svg | 3 --- docs/graphics/interleavings.svg | 3 --- docs/graphics/jpf-abstractions.svg | 3 --- docs/graphics/jpf-basic.svg | 3 --- docs/graphics/jpf-intro-new.svg | 3 --- docs/graphics/jpf-layers.svg | 3 --- docs/graphics/jpf-project.svg | 3 --- docs/graphics/listener-overview.svg | 3 --- docs/graphics/listeners.svg | 3 --- docs/graphics/mji-call.svg | 3 --- docs/graphics/mji-functions.svg | 3 --- docs/graphics/mji-mangling.svg | 3 --- docs/graphics/new-testing.svg | 3 --- docs/graphics/por-mark.svg | 3 --- docs/graphics/por-scheduling-relevance.svg | 3 --- docs/graphics/properties.svg | 3 --- docs/graphics/report.svg | 3 --- docs/graphics/states-mc.svg | 3 --- docs/graphics/states-testing.svg | 3 --- docs/graphics/sw-model-checking-2.svg | 3 --- docs/graphics/sw-model-checking.svg | 3 --- 30 files changed, 90 deletions(-) delete mode 100644 docs/graphics/DFSListener.svg delete mode 100644 docs/graphics/app-types.svg delete mode 100644 docs/graphics/attributes.svg delete mode 100644 docs/graphics/bc-factory.svg delete mode 100644 docs/graphics/cg-impl.svg delete mode 100644 docs/graphics/cg-motivation.svg delete mode 100644 docs/graphics/cg-ontology.svg delete mode 100644 docs/graphics/cg-sequence.svg delete mode 100644 docs/graphics/choicegen-example.svg delete mode 100644 docs/graphics/genpeer.svg delete mode 100644 docs/graphics/interleavings.svg delete mode 100644 docs/graphics/jpf-abstractions.svg delete mode 100644 docs/graphics/jpf-basic.svg delete mode 100644 docs/graphics/jpf-intro-new.svg delete mode 100644 docs/graphics/jpf-layers.svg delete mode 100644 docs/graphics/jpf-project.svg delete mode 100644 docs/graphics/listener-overview.svg delete mode 100644 docs/graphics/listeners.svg delete mode 100644 docs/graphics/mji-call.svg delete mode 100644 docs/graphics/mji-functions.svg delete mode 100644 docs/graphics/mji-mangling.svg delete mode 100644 docs/graphics/new-testing.svg delete mode 100644 docs/graphics/por-mark.svg delete mode 100644 docs/graphics/por-scheduling-relevance.svg delete mode 100644 docs/graphics/properties.svg delete mode 100644 docs/graphics/report.svg delete mode 100644 docs/graphics/states-mc.svg delete mode 100644 docs/graphics/states-testing.svg delete mode 100644 docs/graphics/sw-model-checking-2.svg delete mode 100644 docs/graphics/sw-model-checking.svg diff --git a/docs/graphics/DFSListener.svg b/docs/graphics/DFSListener.svg deleted file mode 100644 index 1684827..0000000 --- a/docs/graphics/DFSListener.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2005-10-21 18:50:44 +0000Canvas 1Layer 1searchStartedsearchFinishedstateAdvancedpropertyViolatedstateBacktrackedsearchConstraintHit diff --git a/docs/graphics/app-types.svg b/docs/graphics/app-types.svg deleted file mode 100644 index f845707..0000000 --- a/docs/graphics/app-types.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2015-01-05 22:17:29 +0000App TypesLayer 1non-functional properties ■ unhandled exceptions (incl. AssertionError) ■ deadlocks ■ racesrestricted choice types ■ scheduling sequences ■ java.util.Random improved inspection ■ coverage statistics ■ exact object counts ■ execution costsconstraintsbenefitsrestricted application models ■ UML statemachines ■ does not run w/o JPF libraries runtime costs ■ order of magnitude slower ■ state storage memorystandard library support ■ java.net, javax.swing, .. (needs abstraction models) functional (domain) properties ■ built-in into JPF librariesfunctional property impl. costs ■ listeners, MJI knowledgeflexible state space ■ domain specific choices (e.g. UML "enabling events")runtime costs & library support ■ usually not a problem, domain libs can control state spaceruns on anyJVMruns onlyunder JPFlow modeling costs ■ statemachine w/o layout hassle,..initial domain impl. costs ■ domain libs can be tricky "sweet spot"annotate program ■ requirements ■ sequences (UML) ■ contracts (PbC) ■ tests … analyze program ■ symbolic exec → test data ■ thread safety / races *.class*.java@V*.javaJPF unawareprogramsJPF enabledprogramsJPF dependentprograms diff --git a/docs/graphics/attributes.svg b/docs/graphics/attributes.svg deleted file mode 100644 index 2aa20a4..0000000 --- a/docs/graphics/attributes.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2011-05-16 18:21:11 +0000Canvas 1Layer 1dup(), push(), pop(), ..------getOperandAttr(idx)setOperandAttr(idx,obj)getLocalAttr(idx)setLocalAttr(idx,obj)int[] localsObject[] localAttrint[] operandsObject[] operandAttrStackFramegetIntValue(idx), ...setIntValue(idx, v), ...------getFieldAttr(idx)setFieldAttr(idx,obj)getObjectAttr()setObjectAttr(obj)int[] valuesObject[] fieldAttrsObject objectAttrFieldslocalsvaluesattributesoperandsslotsfield-valuesattributesputfieldgetfielddup..iload..istore..invokevirtual..return..attributeobjectsetAttr(i,o)getAttr(i)- listener- Instruction- native peerget?Attr(i)set?Attr(i,o)JPF coreJPFextensionattribute APIobject-attrThreadInfoElementInfo diff --git a/docs/graphics/bc-factory.svg b/docs/graphics/bc-factory.svg deleted file mode 100644 index f69c951..0000000 --- a/docs/graphics/bc-factory.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2011-05-16 18:32:22 +0000Canvas 1Layer 1*.classInstruction ifeq(tgt)...«interface»InstructionFactory...Instruction execute()InstructionIFEQIFEQ......Instruction execute (){.. cond = popCondition() if (cond) return jumpTarget else return getNextInsn()setCode(code)factoryInstruction[] codeMethodInfoconcrete execution semanticsabstract execution semanticsconcrete valueexecutionsymbolic valueexecutioninstruction setInstruction execute(){.. if (!firstStepInsn()){ setNextCG(new PCChoiceGenerator()) return this } popCondition() // not interested cond = getCG().getNextChoice() if (cond){... return jumpTarget } else {... return getNextInsn()per bytecodefactory methodsInstruction ifeq(tgt)...gov.nasa.jpf.jvm.bytecodeInstructionFactoryInstruction ifeq(tgt)...gov.nasa.jpf.symbcSymbolicInstructionFactoryInstruction ifeq(int jumpTarget){ return new IFEQ(jumpTarget)ClassInfoClassFileCodeBuilderConfigvm.insn_factory.class=... diff --git a/docs/graphics/cg-impl.svg b/docs/graphics/cg-impl.svg deleted file mode 100644 index 07a14cb..0000000 --- a/docs/graphics/cg-impl.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-02 07:14:49 +0000Canvas 1Layer 1initNextTransition(){... curCg = nextCg nextCg = null curCg.advance() ..setExecThread() ...executeTransition(){.. isFirstStepInsn = true while (pc != null) { nextPc = executeInstruction() if (ss.breakTransition()) break else pc = nextPc isFirstStepInsn = falseexecute(){.. if (!ti.isFirstStepInsn()) { ChoiceGenerator cg = ..createMonitorEnterCG(..) if (cg != null){ ss.setNextChoiceGenerator(cg) return this // repeat } ei.lock(ti) return getNextPc(ti);execute()InstructioninitNextTransition()breakTransition()setNextChoiceGenerator()nextCgcurCgSystemStatehasMoreChoices()advance()ChoiceGeneratorgetNextChoice()threadSetThreadCGgetNextChoice()doubleSetDoubleCG......executeTransition()executeInstruction()isFirstStepInsn(){pc, nextPc}ThreadInfoMonitorEnterInvoke.....MethodInfoNativePeere.g. JPF_gov_nasa_jpf_vm_Verify.getBoolean(env)top half: executed on first invocationoptionally sets next CG and reexecutesbottom half: executed on revisit (orif no CG created because of policy)does semantic action based oncurrent CGs choicescheduling choicesdata acquisition choices123top halfbottomhalfif (!ti.isFirstStepInsn()){ cg = new BooleanCG() ss.setNextChoiceGenerator(cg) env.repeatInvocation() ..} else { cg = ss.getChoiceGenerator() return ((BooleanCG)cg).getNextChoice()}breakTransition(){... return nextCg != null diff --git a/docs/graphics/cg-motivation.svg b/docs/graphics/cg-motivation.svg deleted file mode 100644 index e8c750c..0000000 --- a/docs/graphics/cg-motivation.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2010-02-22 05:27:10 +0000Canvas 1Layer 1T ± Δ.. double v = Verify.getDouble("velocity"); ..velocity.class = gov.nasa.jpf.jvm.choice.DoubleThresholdGeneratorvelocity.threshold = 13250velocity.delta = 500application code(test driver)configuration (e.g. mode property file)C = { T-Δ, T, T+ Δ }Verify.getBoolean()Verify.getInt(0,4)Verify.getDouble(1.0,1.5)C = { true, false }C = { 0, 1, 2, 3, 4 }✓?potentially large sets with lots of uninteresting values??no finite value set without heuristicsC = { ∞ }e.g. "Threshold" heuristicChoice Generators+Configurable Heuristic Choice ModelsJPF internal object to store and enumerate a set of choicesconfigurable classes tocreate ChoiceGenerator instanceshasMoreChoices()advance()getNextChoice() → xchoiceSet: {x}xChoiceGenerator diff --git a/docs/graphics/cg-ontology.svg b/docs/graphics/cg-ontology.svg deleted file mode 100644 index fab55e3..0000000 --- a/docs/graphics/cg-ontology.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2010-02-22 02:58:46 +0000Canvas 1Layer 1TransitionStateChoiceScheduling ChoiceData Choiceboolean b = Verify.getBoolean();double d = Verify.getDouble("MyHeuristic");..synchronized (..) {..}wait (..)x = mySharedObject..Control Choiceif (<cond>) ..INVOKECG.setInvocations(..).. diff --git a/docs/graphics/cg-sequence.svg b/docs/graphics/cg-sequence.svg deleted file mode 100644 index 5e0ff92..0000000 --- a/docs/graphics/cg-sequence.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2006-05-05 17:02:45 +0000Canvas 1Layer 1......get_field...monitor_enter...get_fieldmonitor_enter...ChoiceGeneratorTjTj+1Tj+2CGkCGlsetNextCGgetNextChoiceTransitionc1kc2kc3kSkc1kc2k{{}},==Statebacktrackadvancec2k,c1l...,execute{Instruction}Sl diff --git a/docs/graphics/choicegen-example.svg b/docs/graphics/choicegen-example.svg deleted file mode 100644 index 675ec8d..0000000 --- a/docs/graphics/choicegen-example.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2006-05-03 17:51:17 +0000Canvas 1Layer 1T ± Δ.. double v = Verify.getDouble("velocity"); ..velocity.class = DoubleThresholdvelocity.threshold = 13250velocity.delta = 500application code(test driver)configuration (e.g. mode property file)C = { T-Δ, T, T+ Δ }Verify.getBoolean()Verify.getInt(0,4)Verify.getDouble(1.0,1.5)C = { true, false }C = { 0, 1, 2, 3, 4 }✓?potentially large sets with lots of uninteresting values??no finite value set without heuristicsC = { ∞ }e.g. "DoubleThresholdChoice"Choice Generators+Configurable Heuristic Choice ModelsJPF internal object to store and enumerate a set of choicesconfigurable classes tocreate ChoiceGenerator instanceshasMoreChoices()advance()getNextChoice() → xchoiceSet: {x}xChoiceGenerator diff --git a/docs/graphics/genpeer.svg b/docs/graphics/genpeer.svg deleted file mode 100644 index 6887428..0000000 --- a/docs/graphics/genpeer.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-04 01:29:55 +0000Canvas 1Layer 1GenPeerpackage x.y.z;class MyClass { ... native String foo (int i, String s);}class JPF_x_y_z_MyClass { ... @MJI public static int foo__ILjava_lang_String__2 (MJIEnv env, int objRef, int i, int sRef) { int ref = MJIEnv.NULL; // <2do> fill in body return ref; }}"java gov.nasa.jpf.GenPeer x.y.z.MyClass > JPF_x_y_z_MyClass.java" diff --git a/docs/graphics/interleavings.svg b/docs/graphics/interleavings.svg deleted file mode 100644 index 4dfa19e..0000000 --- a/docs/graphics/interleavings.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-11-19 20:18:08 +0000Canvas 1Layer 1.........12P1P2PNn1n2...AtomicInstructionsThreads12I1∑niIM......nN.........Interleavings(∑ n )!∏ (n !)Ni=1iNi=1iM = diff --git a/docs/graphics/jpf-abstractions.svg b/docs/graphics/jpf-abstractions.svg deleted file mode 100644 index b636c6f..0000000 --- a/docs/graphics/jpf-abstractions.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-11-26 21:24:31 +0000Canvas 1Layer 1search ()VM vmSearchforward ()backtrack ()restoreState ()VMsearch ()DFSearchrun ()search, vm, configJPFexecuteTransition ()executeInstruction ()ThreadInfoinitializeNextTransition()executeNextTransition()SystemStateClassInfoMethodInfoFieldInfoElementInfoFieldsMonitorStaticsbytecode executiontype + codemgntobjectmodelgov.nasa.jpfgov.nasa.jpf.searchsearch ()HeuristicSearchgov.nasa.jpf.vmgov.nasa.jpf.search.heuristicgov.nasa.jpf.vm.bytecodeexecute ()Instruction.........search ()BFSHeuristic...while (notDone) { ..vm.forward(); ..vm.backtrack(); if (!properties.check()){ reportError(); break; ...search.class=...vm.class=...push (), pop() ...StackFrameConfigHeap diff --git a/docs/graphics/jpf-basic.svg b/docs/graphics/jpf-basic.svg deleted file mode 100644 index fdfae11..0000000 --- a/docs/graphics/jpf-basic.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-11-19 18:37:23 +0000Canvas 1Layer 1JPF*.classreport*.jpfSystem under Test(Java bytecode)Verification ResultJPF ConfigurationProperties to Verify diff --git a/docs/graphics/jpf-intro-new.svg b/docs/graphics/jpf-intro-new.svg deleted file mode 100644 index 56fc211..0000000 --- a/docs/graphics/jpf-intro-new.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2009-04-10 01:07:23 +0000Canvas 1Layer 1------------------------------------ error path..Step #14 Thread #1 oldclassic.java:95 event2.waitForEvent(); oldclassic.java:37 wait();------------------------------------ thread stacksThread: Thread-0 at java.lang.Object.wait(Object.java:429) at Event.waitForEvent(oldclassic.java:37) ..======================== 1 Error Found: DeadlockJPFCorebytecodesetlistener/propertypublisher/ -extchoicegeneratorserializer/restorerannotation (optional) in-sourceproperty specdomainframeworkmodellibraryapplicationSuTexecutionenvironmentsearchstrategyJavavirtualmachinebytecodereportJPFendseenerror-pathproperty violationhost - JVMJPF distribution...nativepeer......extensions*.jpfJPF configurationreportstandardJava libraries*.jar*.jar diff --git a/docs/graphics/jpf-layers.svg b/docs/graphics/jpf-layers.svg deleted file mode 100644 index ada4957..0000000 --- a/docs/graphics/jpf-layers.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-02 21:48:18 +0000Canvas 1Layer 1platform OShost JVMnative librarieslibrary classesJPF (Java application)modeled classesrt.jarJNIMJI*.classsystem under teststandard Java installationCLASSPATHModel layerJava layerNative layer"Java Native Interface""Model Java Interface" diff --git a/docs/graphics/jpf-project.svg b/docs/graphics/jpf-project.svg deleted file mode 100644 index 790b51b..0000000 --- a/docs/graphics/jpf-project.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2009-09-09 23:36:00 +0000Canvas 1Layer 1jpf-Xsrcbuildbuild.xmljpf.propertiesX.jarX-classes.jarX-annotations.jarmainpeersclassesannotationstestsexampleslibtoolsbinRunJPF.jarRunAnt.jarjpfantnbprojectproject.xmlide-file-targets.xml.classpathmainpeersclassesannotationstestsexampleseclipserun-jpf.launchJPF project properties file(runtime def: native_classpath, classpath, sourcepath)host-VM executed classes (listeners, infrastructure etc.)host-VM executed library classes (MJI native peers)JPF executed library classes →sourcepathJPF processed Java annotationsregression testsdemos →sourcepathAnt build script (compile, build, test, clean)temporary build artifacts (classfiles)main host-VM executed project jar (main,peers →native_classpath)JPF executed library jar (classes,annotations →classpath)separate anotations jar (for JPF external SUT exec)required runtime jars →native_classpathbuild toolsant.jar, junit.jar, ...bcel.jar, antlr.jar, ..(example) 3rd party jarsbuild artifactspermanent build artifacts(example) 3rd party jarsJPF startup jar (executable)JPF build jar (executable)scriptsJPF startup script (→RunJPF.jar)JPF build script (→RunAnt.jar)Eclipse project configurationproject sourcesproject root directorybinary distributionNetBeans project configurationNetBeans file actions (JPF execution)Eclipse launch configs (JPF execution)IDE supportcompilebuildtest diff --git a/docs/graphics/listener-overview.svg b/docs/graphics/listener-overview.svg deleted file mode 100644 index 8a58bd9..0000000 --- a/docs/graphics/listener-overview.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-02 07:42:37 +0000Canvas 1Layer 1SearchVMJPFSystem under testlistenersexecuted by JPFexecuted by host JVMsearch event notificationsexecution event notificationsconfigured- classLoaded (vm)- threadScheduled (vm)- threadNotified (vm) ...- executeInstruction (vm)- instructionExecuted (vm) ...- objectCreated (vm) ...- exceptionThrown(vm) ...- choiceGeneratorAdvanced (vm) ...- stateAdvanced (search)- stateBacktracked (search)- propertyViolated (search)- searchFinished (search) ...- +listener=<listener-class>- @JPFConfig(..)- listener.autoload=<annotations>- jpf.addListener(..) ...≪SearchListener≫≪VMListener≫ diff --git a/docs/graphics/listeners.svg b/docs/graphics/listeners.svg deleted file mode 100644 index 681d1ad..0000000 --- a/docs/graphics/listeners.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2009-04-08 19:52:28 +0000Canvas 1Layer 1«interface»JPFListenerexecuteInstruction(vm)instructionExecuted(..)threadStarted(..)objectCreated(..)choiceGeneratorSet(..)choiceGeneratorAdvanced(..). . .«interface»VMListenersearchStarted(search)stateAdvanced(..)stateBacktracked(..)propertyViolated(..)searchFinished(..). . .«interface»SearchListenercheck(search,vm)getErrorMessage()«interface»Propertycheck(search,vm) {}. . .GenericPropertyinstructionExecuted(vm) {}searchStarted(search) {}. . .ListenerAdapterpublishStart(publisher)publishFinished(..). . .«interface»PublisherExtensioninstructionExecuted(vm) {}searchStarted(search) {}. . .PropertyListenerAdapter diff --git a/docs/graphics/mji-call.svg b/docs/graphics/mji-call.svg deleted file mode 100644 index d5db418..0000000 --- a/docs/graphics/mji-call.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2011-05-24 04:08:50 +0000Canvas 1Layer 1package x.y.z;class C { ... native int foo (int p);}class JPF_x_y_z_C { ... public static int foo__I__I (MJIEnv env, int thisRef, int p) { int d = env.getIntField(thisRef, "data"); .. }}...int a = c.foo(3);...aload_1icont_3invokevirtual ..executeMethod (ThreadInfo ti..){ MJIEnv env = ti.getMJIEnv(); Object[] args = getArguments(); .. mth.invoke(peerCls, args); ..}ClassInfo (..){ peerCls = loadNativePeer(..); ..}executeMethod()peerClsClassInfoexecuteMethod()methodsNativePeergetXField(..)setXField(..)...threadInfoMJIEnvenvThreadInfoJPFclassloadingJPFmethodinvocationJPFobjectaccessJPF (model) classJVM (Java) classJava reflection callreflection diff --git a/docs/graphics/mji-functions.svg b/docs/graphics/mji-functions.svg deleted file mode 100644 index bac9b5c..0000000 --- a/docs/graphics/mji-functions.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2011-05-24 04:01:26 +0000Canvas 1Layer 1class JPF_x_y_z_MyClass { public static int foo__ILjava_lang_String_2__Ljava_lang_String_2 (MJIEnv env, int objRef, int i, int sRef) { String s = env.getStringObject(sRef); .. int ref = env.newString(..); return ref; }}package x.y.z;class MyClass { .. native String foo (int i, String s);}MJIEnvJPF objectsJava objectsNativePeerJPF executedhost VM executed- method lookup- parameter conversion- invocation- field access- object conversion- JPF intrinsics access"Model" Class"NativePeer" ClassMJI - "Model Java Interface" diff --git a/docs/graphics/mji-mangling.svg b/docs/graphics/mji-mangling.svg deleted file mode 100644 index 7e59270..0000000 --- a/docs/graphics/mji-mangling.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-02 21:54:02 +0000Canvas 1Layer 1package x.y;class MyClass { native int foo (int i, String s);}class JPF_x_y_MyClass { public static int foo__ILjava_lang_String_2 (MJIEnv env, int objref, int i, int sRef) {..}}Model ClassNative Peer Classmodel parameters(refs become 'int')MJI parametersJNI conformant manglingbooleanbytecharshortintlongfloatdoubleZBCSIJFD'_'';''['_1_2_3<type> [][<type>x.y.ZLx_y_Z_2<func> (..)<func>__<signature> diff --git a/docs/graphics/new-testing.svg b/docs/graphics/new-testing.svg deleted file mode 100644 index 4254ad1..0000000 --- a/docs/graphics/new-testing.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-05 00:34:03 +0000Canvas 1Layer 1@Test public void testX() { if (verifyNoPropertyViolation()) { String s = "one" + " two"; assert "one two".equals(s); }}boolean verifyNoPropertyViolation (String... jpfArgs) { ... args = append(jpfArgs, caller.getClassName(), caller.getMethodName()); .. JPF jpf = createAndRunJPF(args); ... errors = jpf.getSearchErrors(); if (!errors.isEmpty()) throw new AssertionError(..); ... return false; // -> don't execute test block}boolean verifyNoPropertyViolation(..){ return true;}start()JPFShellrunTestsOfThisClass()createAndRunJPF()...verifyNoPropertyViolation()verifyPropertyViolation()verifyUnhandledException()verifyAssertionError()...TestJPFtestX()...MyJPFProjectTestjpf-coretested JPF projectverifyNoPropertyViolation()verifyPropertyViolation()verifyUnhandledException()verifyAssertionError()JPF_.._TestJPFnative peercode verified by JPFexecuted by JPF whenrunning testexecuted outside JPF (starting JPF on test) diff --git a/docs/graphics/por-mark.svg b/docs/graphics/por-mark.svg deleted file mode 100644 index f47b060..0000000 --- a/docs/graphics/por-mark.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-12-02 07:35:36 +0000Canvas 1Layer 1XX1XX12Xstatic fieldsT1T2root setheapphase 1phase 21 & 2 : referencing thread numberX : shared diff --git a/docs/graphics/por-scheduling-relevance.svg b/docs/graphics/por-scheduling-relevance.svg deleted file mode 100644 index 45c2886..0000000 --- a/docs/graphics/por-scheduling-relevance.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2011-05-11 18:17:44 +0000Canvas 1Layer 1executed bytecode instructionfield insnsync insninvoke insnsync mththreading callscheduling relevant insn typeother runnable threadsrecursive locksshared objectslock protected accessscheduling relevant instruction (registeres a ThreadChoiceGenerator)data racesdeadlocks(lock races)tracking of access threadslock distance & statisticsThread. start(), yield() sleep(), join()Object.wait(),notify()configuredclass/mthdattributesGETFIELDPUTFIELDGETSTATICPUTSTATICxALOADxASTOREMONITORENTERMONITOREXITINVOKEVIRTUALINVOKESTATIC diff --git a/docs/graphics/properties.svg b/docs/graphics/properties.svg deleted file mode 100644 index ad56b87..0000000 --- a/docs/graphics/properties.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2011-05-11 18:07:23 +0000Canvas 1Layer 1jpf.home = ${user.home}/projects/jpfjpf-core = ${jpf.home}/jpf-corejpf-awt = ${jpf.home}/awtjpf-shell = ${jpf.home}/jpf-shelljpf-aprop = ......extensions = ${jpf-core},${jpf-shell}jpf-core = ${config_path}jpf-core.native_classpath=\ ${jpf-core}/build/jpf.jar;\ ... ${jpf-core}/lib/bcel.jar;jpf-core.classpath=\ build/jpf-classes.jarjpf-core.test_classpath=\ build/testsjpf-core.sourcepath=\ src/classes...jpf-awt-shell = ${config_path}@using = jpf-awtjpf-awt-shell.native_classpath=...jpf-awt-shell.classpath=......target = RobotManagertarget_args = ...@using = jpf-aprop@import = ./my.propertiesshell = .shell.basicshell.BasicShelllistener = .aprop.listener.SharedChecker...1. site properties2. project properties3. application properties4. command line~/.jpf/site.properties<project>/jpf.properties<project>/.../*.jpf> bin/jpf [-log][-show] {+log.info=..} .../RobotManager.jpf all jpf.properties inorder of extensionsjpf.properties in current directory- project locations- pre-loaded projects- project class paths- project dependencies- system-under-test- listeners, shells- debuggingcommand line property arguments...applicationpropertiessite properties diff --git a/docs/graphics/report.svg b/docs/graphics/report.svg deleted file mode 100644 index cad3324..0000000 --- a/docs/graphics/report.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2010-09-10 23:02:45 +0000Canvas 1Layer 1JPF()addPublisherExtension()setPublisherTopics()reporterJPF..reporter = config.getInstance("report.class", Reporter.class,..);..searchStarted()propertyViolated()searchFinished()publishersReporterpublishStart()getOut()extensionstopicsoutPublisherpublishStart()publishTransition()publishPropertyViolation()publishFinished()<<PublisherExtension>>........for (Publisher p : publishers){ p.openChannel(); .. p.publishStart();.. public void publishStart() { for (String topic : startTopics) { if ("jpf".equals(topic)){ publishJPF(); ... for (PublisherExtension e : extensions) { e.publishStart(this); } ...out.println("JPF version" + ..);publishJPF()...ConsolePublisherpublishFinished()...DeadlockAnalyzerPrintWriter out = publisher,getOut();printTraceAnalysis(out);data collectionpublisher managementdata formattingtopic managementoutput channel managementproperty/listenerspecific output topicsreport.class=.report.Reporterreport.publisher=console,..report.console.class=.report.ConsolePublisherreport.console.start=jpf,..JPF configuration(e.g. jpf.properties or *.jpf files) diff --git a/docs/graphics/states-mc.svg b/docs/graphics/states-mc.svg deleted file mode 100644 index 8d9f5fd..0000000 --- a/docs/graphics/states-mc.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2009-09-06 18:37:27 +0000Canvas 1Layer 1☠model checking:all program state are explored until none left or defect foundbacktrack≡≡≡match✘ diff --git a/docs/graphics/states-testing.svg b/docs/graphics/states-testing.svg deleted file mode 100644 index 12e5396..0000000 --- a/docs/graphics/states-testing.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-11-19 20:33:35 +0000Canvas 1Layer 1☠based on input set {d}only one pathexecuted at a time✔testing:{d} diff --git a/docs/graphics/sw-model-checking-2.svg b/docs/graphics/sw-model-checking-2.svg deleted file mode 100644 index a0575f7..0000000 --- a/docs/graphics/sw-model-checking-2.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2015-01-05 22:19:29 +0000Canvas 1Layer 1a=0b=0b=1b=2c=0c=0c=0/0starta=1b=0b=1b=2c=-1c=1/0c=1✘12345✔✔6 diff --git a/docs/graphics/sw-model-checking.svg b/docs/graphics/sw-model-checking.svg deleted file mode 100644 index 1fd0a54..0000000 --- a/docs/graphics/sw-model-checking.svg +++ /dev/null @@ -1,3 +0,0 @@ - - - Produced by OmniGraffle 6.1 2014-11-19 20:40:12 +0000Canvas 1Layer 1Random random = new Random() int a = random.nextInt(2)int b = random.nextInt(3)int c = a/(b+a -2)①②③④a=0b=0b=1b=2c=0c=0c=0/0starta=1b=0b=1b=2c=-1c=1/0c=1✔ -- 2.34.1