Questo è il comando lpssuminst che può essere eseguito nel provider di hosting gratuito OnWorks utilizzando una delle nostre molteplici workstation online gratuite come Ubuntu Online, Fedora Online, emulatore online Windows o emulatore online MAC OS
PROGRAMMA:
NOME
lpssuminst - istanzia le variabili di sommatoria di un LPS
SINOSSI
lpssuminst [OPZIONE]... [INFILE [PROFILO]]
DESCRIZIONE
Istanziare le variabili di sommatoria della specifica del processo lineare (LPS) in INFILE
e scrivi il risultato in OUTFILE. Se INFILE non è presente, viene utilizzato stdin. Se OUTFILE è
non presente, viene utilizzato stdout.
VERSIONI
OPZIONE può essere uno dei seguenti:
-f, --finito
istanziare solo variabili i cui tipi sono finiti
-QNUM, --qlimit=NUM
limitare l'enumerazione dei quantificatori a variabili NUM. (Predefinito NUM=1000, NUM=0 per
illimitato).
-rNOME, --riscrittore=NOME
usa la strategia di riscrittura NAME: 'jitty' jitty rewriting (predefinito) 'jittyc' compilato
riscrittura jitty 'jittyp' riscrittura jitty con prover
-s[NOME], --sort[=NOME]
seleziona gli ordinamenti che devono essere espansi (elenco separato da virgole)
Esempi: Bool; Bool, Elenco (Nat)
-t, --tau
istanziare solo le variabili nei riassunti tau
--tempi[=RISORSE]
aggiungere le misurazioni dei tempi a FILE. Le misurazioni vengono scritte nell'errore standard se
non viene fornito alcun FILE
Opzioni standard:
-q, --silenzioso
non visualizzare messaggi di avviso
-v, --verboso
visualizzare brevi messaggi intermedi
-d, - debug
visualizzare messaggi intermedi dettagliati
--livello-log=LIVELLO
visualizzare messaggi intermedi fino al livello compreso
-h, --Aiuto
visualizzare le informazioni di aiuto
--versione
visualizzare le informazioni sulla versione
Utilizzare lpssuminst online utilizzando i servizi onworks.net
