Proof RESTARTS_ROUTINE (#251) (#327)

Proof RESTARTS_ROUTINE (closes #251)
pull/337/head
cai 2018-04-23 22:32:55 +08:00 committed by James Harris
parent b66290c2e6
commit a6693fd688
1 changed files with 26 additions and 24 deletions

View File

@ -53,11 +53,11 @@ RESTARTS CA MPAC +5 # GET GROUP NUMBER -1
CA TEMPPHS
MASK OCT1400
CCS A # IS IT A VARIABLE OR TABLE RESTART
TCF ITSAVAR # IT'S A VARIABLE RESTART
TCF ITSAVAR # IT:S A VARIABLE RESTART
GETPART2 CCS TEMPPHS # IS IT AN X.1 RESTART
CCS A
TCF ITSATBL # NO, IT'S A TABLE RESTART
TCF ITSATBL # NO, ITS A TABLE RESTART
CA PRIO14 # IT IS AN X.1 RESTART, THEREFORE START
TC FINDVAC # THE DISPLAY RESTART JOB
@ -68,9 +68,9 @@ GETPART2 CCS TEMPPHS # IS IT AN X.1 RESTART
ITSAVAR MASK OCT1400 # IS IT TYPE B ?
CCS A
TCF ITSLIKEB # YES, IT IS TYPE B
TCF ITSLIKEB # YES,IT IS TYPE B
EXTEND # STORES THE JOB (OR TASK) 2CADR FOR EXIT
EXTEND # STORE THE JOB (OR TASK) 2CADR FOR EXIT
NDX TEMP2G
DCA PHSNAME1
DXCH GOLOC
@ -79,13 +79,13 @@ ITSAVAR MASK OCT1400 # IS IT TYPE B ?
MASK OCT7
AD MINUS2
CCS A
TCF ITSLNGCL # IT'S A LONGCALL
TCF ITSLNGCL # ITS A LONGCALL
# Page 1415
RTRNCADR TC SWRETURN # CAN'T GET HERE.
RTRNCADR TC SWRETURN # CANT GET HERE
TCF ITSAWAIT
TCF ITSAJOB # IT'S A JOB
TCF ITSAJOB # ITS A JOB
ITSAWAIT CA WTLTCADR # SET UP WAITLIST CALL
TS GOLOC -1
@ -109,7 +109,7 @@ TIMETEST CCS A # IS IT AN IMMEDIATE RESTART
COUNT 02/RSROU
ITSINDIR LXCH GOLOC +1 # GET THE CORRECT E BANK IN CASE THIS IS
LXCH BB # SWITCHED ERASABLE
LXCH BB # SWITCHED ERRASIBLE
NDX A # GET THE TIME INDIRECTLY
CA 1
@ -156,19 +156,19 @@ ITSLIKEB CA RTRNCADR # TYPE B, SO STORE RETURN IN
TS TEMPPHS
EXTEND
NDX TEMP2G # OBTAIN THE JOB'S 2CADR
NDX TEMP2G # OBTAIN THE JOB:S 2CADR
DCA PHSNAME1
DXCH GOLOC
ITSAJOB NDX TEMP2G # NOW ADD THE PRIORITY AND LET'S GO
ITSAJOB NDX TEMP2G # NOW ADD THE PRIORITY AND LET:S GO
CA PHSPRDT1
CHKNOVAC TS GOLOC -1 # SAVE PRIO UNTIL WE SEE IF IT'S
CHKNOVAC TS GOLOC -1 # SAVE PRIO UNTIL WE SEE IF ITS
EXTEND # A FINDVAC OR A NOVAC
BZMF ITSNOVAC
CAF FVACCADR # POSITIVE, SET UP FINDVAC CALL.
XCH GOLOC -1 # PICK UP PRIO
TC GOLOC -1 AND GO
XCH GOLOC -1 # PICK UP PRIO,
TC GOLOC -1 # AND GO
ITSNOVAC CAF NOVACADR # NEGATIVE,
XCH GOLOC -1 # SET UP NOVAC CALL,
@ -177,7 +177,7 @@ ITSNOVAC CAF NOVACADR # NEGATIVE,
ITSATBL TS CYR # FIND OUT IF THE PHASE IS ODD OR EVEN
CCS CYR
TCF +1 # IT'S EVEN
TCF +1 # IT:S EVEN
TCF ITSEVEN
CA RTRNCADR # IN CASE THIS IS THE SECOND PART OF A
@ -201,7 +201,7 @@ CONTBL2 EXTEND # FIND OUT WHAT'S IN THE TABLE
TCF ITSAJOB2
INCR A # MUST BE EITHER A WAITLIST OR LONGCALL
TS GOLOC # LET'S STORE THE CORRECT CADR
TS GOLOC # LET-S STORE THE CORRECT CADR
CA WTLTCADR # SET UP OUR EXIT TO WAITLIST
TS GOLOC -1
@ -210,7 +210,7 @@ CONTBL2 EXTEND # FIND OUT WHAT'S IN THE TABLE
MASK BIT10 # THIS SHOULD BE ONE IF WE HAVE -BB
CCS A # FOR THAT MATTER SO SHOULD BE BITS 9,8,7,
# 6,5, AND LAST BUT NOT LEAST (PERHAPS NOT
# IN IMPORTANCE ANYWAY. BUT 4
# IN IMPORTANCE ANYWAY. BIT 4
TCF ITSWTLST # IT IS A WAITLIST CALL
NDX POINTER # OBTAIN THE ORIGINAL DELTA T
@ -237,7 +237,8 @@ ITSLGCL1 LXCH GOLOC +1 # OBTAIN THE CORRECT E BANK
LXCH GOLOC +1 # RESTORE OUR E AND F BANK
LXCH BB # RESTORE THE TASKS E AND F BANKS
LXCH GOLOC +1 # AND PRESERVE OUR L
TCF ITSLGCL2 # NOT GET'S PROCESS THIS LONGCALL
TCF ITSLGCL2 # NOW LET:S PROCESS THIS LONGCALL
# ***** YOU MAY RETURN TO SWITCHED FIXED *****
@ -246,6 +247,7 @@ ITSLGCL1 LXCH GOLOC +1 # OBTAIN THE CORRECT E BANK
BANK
COUNT 01/RSROU
ITSLGCL2 DXCH LONGTIME
EXTEND # CALCULATE TIME LEFT
@ -261,7 +263,7 @@ ITSLGCL2 DXCH LONGTIME
TCF IMEDIATE -3
CCS LONGTIME +1
TCF LONGCLCL
NOOP # CAN'T GET HERE ************
NOOP # CAN:T GET HERE *********
TCF IMEDIATE -3
TCF IMEDIATE
@ -290,30 +292,30 @@ ITSWTLST CS GOLOC +1 # CORRECT THE BBCON INFORMATION
ITSAJOB2 XCH GOLOC # STORE THE CADR
NDX POINTER # ADD THE PRIORITY AND LET'S GO
NDX POINTER # ADD THE PRIORITY AND LET:S GO
CA PRDTTAB
TCF CHKNOVAC
ITSEVEN CA TEMPSWCH # SET FOR EITHER THE SECOND PART OF THE
ITSEVEN CA TEMPSWCH # SET UP FOR EITHER THE SECOND PART OF THE
TS GOLOC +2 # TABLE, OR A RETURN FOR THE NEXT GROUP
NDX TEMP2G # SET UP POINTER FOR OUR LOCATION WITHIN
CA SIZETAB # THE TABLE
AD TEMPPHS # THIS MAY LOOK BAD BUT LET'S SEE YOU DO
AD TEMPPHS # THIS MAY LOOK BAD BUT LET:S SEE YOU DO
AD TEMPPHS # BETTER IN TIME OR NUMBER OF LOCATIONS
AD TEMPPHS
TS POINTER
TCF CONTBL2 # NO PROCESS WHAT IS IN THE TABLE
TCF CONTBL2 # NOW PROCESS WHAT IS IN THE TABLE
PHSPART2 CA THREE # SET THE POINTER FOR THE SECOND HALF OF
ADS POINTER # THE TABLE
CA RTRNCADR # THIS WILL BE OUR LAST TIME THROUGH THE
TS GOLOC +2 # EVEN TABLE, SO AFTER IT GET THE NEXT
TS GOLOC +2 # EVEN TABLE , SO AFTER IT GET THE NEXT
# GROUP
TCF CONTBL2 # SO LET'S GET THE SECOND ENTRY IN THE TBL
TCF CONTBL2 # SO LET:S GET THE SECOND ENTRY IN THE TBL
TEMPPHS EQUALS MPAC
TEMP2G EQUALS MPAC +1